DEV Community

Cover image for Dependent Types in PureScript
Mike Solomon
Mike Solomon

Posted on • Updated on

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


Enter fullscreen mode Exit fullscreen mode

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 = []


Enter fullscreen mode Exit fullscreen mode

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)


Enter fullscreen mode Exit fullscreen mode

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


Enter fullscreen mode Exit fullscreen mode

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)


Enter fullscreen mode Exit fullscreen mode

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)


Enter fullscreen mode Exit fullscreen mode

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


Enter fullscreen mode Exit fullscreen mode

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


Enter fullscreen mode Exit fullscreen mode

Now, we can get something that almost resembles the Idris result in PureScript:



a = mkSingle true show
b = mkSingle false show


Enter fullscreen mode Exit fullscreen mode

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


Enter fullscreen mode Exit fullscreen mode

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


Enter fullscreen mode Exit fullscreen mode

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


Enter fullscreen mode Exit fullscreen mode

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


Enter fullscreen mode Exit fullscreen mode

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


Enter fullscreen mode Exit fullscreen mode

And because discard is just a special case of bind, we can do:



discard = bind


Enter fullscreen mode Exit fullscreen mode

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


Enter fullscreen mode Exit fullscreen mode

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


Enter fullscreen mode Exit fullscreen mode

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!


Enter fullscreen mode Exit fullscreen mode

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!


Enter fullscreen mode Exit fullscreen mode

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.

Graph of code quality versus understandability

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)

Collapse
 
srghma profile image
Serhii Khoma

can You please write about Calculus of Constructions and lambda cube? (have no idea what is this) O_O 🙏