Dependent Types in PureScript

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:

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 js 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:

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.