I've seen a bit of chatter recently in the PS community about dependent types. Many of us that have been using PureScript for years love it because of its simplicity and elegance, and there has been resistance in the community to build out the complexity, both syntax-wise and implementation-wise, of a full-blown dependently-typed language ร la Idris and Agda.
But another reason that there's not much community momentum behind adding dependent types to PureScript is because PureScript already has dependent types ๐
To see them in action, let's consider the following example from the Idris documentation:
In Idris, types are first class, meaning that they can be computed and manipulated (and passed to functions) just like any other language construct. For example, we could write a function which computes a type:
isSingleton : Bool -> Type
isSingleton True = Nat
isSingleton False = List Nat
This function calculates the appropriate type from a Bool which flags whether the type should be a singleton or not. We can use this function to calculate a type anywhere that a type can be used. For example, it can be used to calculate a return type:
mkSingle : (x : Bool) -> isSingleton x
mkSingle True = 0
mkSingle False = []
The Idris docs present us with a classic, bread-and-butter dependent type. The "hello world" of dependent types if you will. As a reminder:
Input | Output | Name | Example |
---|---|---|---|
Term | Term | Function | not true -- false |
Type | Term | Typeclass | emptyString = mempty @String |
Type | Type | Functional dependency | forall t. Generic Foo t |
Term | Type | Dependent type | See above |
In PureScirpt, if you define isSingleton
and mkSingle
using identical syntax to Idris, you'll get an error. You simply can't put a term in and get a type out. Or can you ๐
Continuation
Going back to the Idris example, let's assume that you have a result of mkSingle True
or mkSingle False
. What type is the result? It depends! But what can we do with the term that inhabits this nebulous type? We can only do actions that are defined on all possible outcomes of mkSingle
. This is where a more familiar concept comes in - typeclasses, aka instances in Idris.
For example, we can do:
a = show (mkSingle True)
b = show (mkSingle False)
Here, the compiler is smart enough to pick the instance of show
that corresponds to the output type of mkSingle
.
Another way to say this is that show
continues our program.
One neat trick in functional programming is that continuations can be passed around like anything else - values, functions, etc. There's even a fancy name for it: Continuation Passing Style, or CPS.
Can CPS get us a serviceable equivalent mkSingle
in PureScript? Let's see.
First, let's define a typeclass called MkSingle
that has a continuation baked into it:
class MkSingle i where
mkSingle :: i -> (forall j. MkSingle j => j -> String) -> String
We give mkSingle
a value i
, and then a continuation that works on all j
s for which MkSingle
is implemented (including potentially i
). At the end, we expect this to output a String
.
This isn't that different from the definition of Cont
in PureScript, which is a classic continuation type:
newtype Cont r a = ((a -> r) -> r)
The only difference between MkSingle
and Cont
is that first term of type i
. This will be the term that our dependent type "depends" on.
Now, let's define a mkSingle
like the Idris example, except instead of returning a type, we'll feed that type to a continuation.
instance MkSingle Boolean where
mkSingle true c = c 0
mkSingle false c = c (Nil@Int)
If you compile this, it will fail because there is no instance of MkSingle Int
nor MkSingle (List Int)
. To use dependent types in PureScript, we need to bake that computational context into our type system. There are several ways to do that, one of which is to use instance chains
else Show i => instance MkSingle i where
mkSingle i _ = show i
To recreate Idris example above where show
is used, we can require that all inhabitants of MkSingle
also implement Show
:
class Show i <= MkSingle i where
mkSingle :: i -> (forall j. MkSingle j => j -> String) -> String
Now, we can get something that almost resembles the Idris result in PureScript:
a = mkSingle true show
b = mkSingle false show
It's a bit backwards (CPS always is), but it does the job!
Making it look like a program
Now that we've found a neat little dependent type trick in PureScript, we decide to go to town with all sorts of term-dependent branching logic:
data Outcome = TheJigIsUp | BrokeFree
instance Show Outcome where
show TheJigIsUp = "The jig is up!"
show BrokeFree = "Broke free!"
class Show i <= MkSingle i where
mkSingle :: i -> (forall j. MkSingle j => j -> String) -> String
instance MkSingle Boolean where
mkSingle true c = c 0
mkSingle false c = c (Nil@Int)
else instance MkSingle Int where
mkSingle 0 c = c 42.0
mkSingle _ c = c $ Just unit
else instance MkSingle Number where
mkSingle 42.0 c = c (Nothing@Unit)
mkSingle _ c = c 15
else instance MkSingle (List Int) where -- Boolean
mkSingle Nil c = c 42
mkSingle _ c = c 0
else instance MkSingle String where -- String
mkSingle s _ = s
else instance MkSingle (Maybe Unit) where
mkSingle (Just _) c = c TheJigIsUp
mkSingle _ c = c BrokeFree
else instance Show i => MkSingle i where
mkSingle i _ = show i
The first branch on true
/false
is exactly what we saw before to recreate the Idris
example, but now there are a bunch other branches well. Can you blame us? Dependent types are like Pringles...
All well and good, but let's say we want to write a program using these.
program :: String
program i = mkSingle i
\a -> mkSingle a
\b -> mkSingle b
\c -> mkSingle c
\d -> mkSingle d show
Yikes. No one likes the look of that. Thankfully, PureScript has rebindable do
notation that allows one to redefine bind
and discard
to get prettier syntax. Before defining them, let's see what that affords us:
program :: Boolean -> String
program i = Dep.do
a <- mkSingle i
b <- mkSingle a
c <- mkSingle b
d <- mkSingle c
show d
Now that's more like it! Let's chase the types and terms when we pass in true
vs false
for i
:
i |
a |
a 's Type
|
b |
b 's Type
|
c |
c 's Type
|
d |
d 's Type
|
---|---|---|---|---|---|---|---|---|
true |
0 |
Int |
42.0 |
Number |
Nothing |
Maybe Unit |
TheJigIsUp |
Outcome |
false |
Nil |
List Int |
42 |
Int |
Just unit |
Maybe Unit |
BrokeFree |
Outcome |
Now if that's not types depending on terms, aka dependent types, I'll eat my fedora!
But what bind
will get us this outcome? Each invocation of mkSingle
gives us a result of (forall j. MkSingle j => j -> String) -> String
. Each left-bind is a continuation of type forall j. MkSingle j => j -> String
. And the whole thing produces a String
. So we can define bind
as.
bind ::
-- outcome of mkSingleton
((forall j. MkSingle j => j -> String) -> String) ->
-- continuation
(forall j. MkSingle j => j -> String) ->
-- result
String
If you squint hard enough, you can see that what's going into the function bind
is coming out of it (add some parentheses around the second half if it makes it easier). So really, we can just define bind
as:
bind :: forall a. a -> a
bind = identity
And because discard
is just a special case of bind
, we can do:
discard = bind
Voilร ! Here's the whole shebang:
module Dep where
import Prelude hiding (bind, discard)
import Data.List (List(..))
import Data.Maybe (Maybe(..))
data Outcome = TheJigIsUp | BrokeFree
instance Show Outcome where
show TheJigIsUp = "The jig is up!"
show BrokeFree = "Broke free!"
class Show i <= MkSingle i where
mkSingle :: i -> (forall j. MkSingle j => j -> String) -> String
instance MkSingle Boolean where
mkSingle true c = c 0
mkSingle false c = c (Nil @Int)
else instance MkSingle Int where
mkSingle 0 c = c 42.0
mkSingle _ c = c $ Just unit
else instance MkSingle Number where
mkSingle 42.0 c = c (Nothing @Unit)
mkSingle _ c = c 15
else instance MkSingle (List Int) where -- Boolean
mkSingle Nil c = c 42
mkSingle _ c = c 0
else instance MkSingle String where -- String
mkSingle s _ = s
else instance MkSingle (Maybe Unit) where
mkSingle (Just _) c = c TheJigIsUp
mkSingle _ c = c BrokeFree
else instance Show i => MkSingle i where
mkSingle i _ = show i
bind :: forall a. a -> a
bind = identity
discard :: forall a. a -> a
discard = bind
Taking it for a spin.
What fun would dependent types be without building an amazing, production-ready application with them? Because that's what we functional programmers do, right? We don't spend time in lofty ivory towers contemplating the CurryโHoward correspondence. We ship software. Right? Of course right!
Let's write the following main
function. It'll read from the console and then invoke our dependently-typed program with true
if it gets "true"
and false
otherwise. This is the true litmus test of dependent types: the compiler can't cheat by finding a term in the source code. This isn't Java. The incoming term is completely controlled by the invoker of the CLI.
module Main where
import Prelude
import Dep (mkSingle)
import Dep as Dep
import Effect (Effect)
import Effect.Aff (launchAff_)
import Effect.Class (liftEffect)
import Effect.Class.Console (log)
import Node.ReadLine (close, createConsoleInterface, noCompletion)
import Node.ReadLine.Aff (question)
program :: Boolean -> String
program i = Dep.do
a <- mkSingle i
b <- mkSingle a
c <- mkSingle b
d <- mkSingle c
show d
main :: Effect Unit
main = launchAff_ do
console <- liftEffect $ createConsoleInterface noCompletion
response <- question "Type something truthy: " console
log $ program (if response == "true" then true else false)
liftEffect $ close console
Now let's run it!
mikesol@Mikes-MacBook-Pro dep % pnpm spago run
Reading Spago workspace configuration...
โ
Selecting package to build: dep
Downloading dependencies...
Building...
Src Lib All
Warnings 0 0 0
Errors 0 0 0
โ
Build succeeded.
Type something truthy: true
Broke free!
Yesssss. Now let's try again:
mikesol@Mikes-MacBook-Pro dep % pnpm spago run
Reading Spago workspace configuration...
โ
Selecting package to build: dep
Downloading dependencies...
Building...
Src Lib All
Warnings 0 0 0
Errors 0 0 0
โ
Build succeeded.
Type something truthy: false
The jig is up!
Drats. And there you have it, dependent types in PureScript.
But seriously, do we actually want these things? To close, I'll present a curve. On the X axis is "type spiciness", with 0 on the left (JavaScript
) and 10 on the right (coq
). On the Y-axis are two curves: the green one represents what percentage of developers can grok your code in less than 10 minutes, and the red one represents the caliber of code you're likely to produce.
In other words, for me, dependent types is an inflection point where you don't get much better software, but you exclude a giant chunk of the community that simply can't follow the control flow of your software because "it depends." You have to think like a compiler to hold that state in your head, which few of us want to do. The whole reason we use compilers is to not have to think like them.
So, even though I <3 dependent types, I'm not putting them in my production code anytime soon. Mostly, I wanted to write this article to show that a robust type system like PureScript (and many others) can accommodate many flavors of dependent types, even if it's not anywhere near the Calculus of Constructions on the lambda cube.
Top comments (1)
can You please write about Calculus of Constructions and lambda cube? (have no idea what is this) O_O ๐