The Dialectics of Type-Level Programming; or How I Learned To Love Values

¡Hola!

thank you

Soy Aaron Levin

@aaronmblevin

today

we are going to do great things

1. DSLs
2. Type-Level DSLs
3. Example
4. A Type-Level DSL for Event Processing
5. The Pains of Being Pure at Heart

DSL

Domain

Specific

Language

GNU make

Verilog

eDSL

embedded

Domain

Specific

Language

eDSL

Value

Domain-Specific

Meaning

combinators

eDSLs are not extensible

​

:( :( :(

Type-Level DSL

Type-Level DSL

Value

Domain-Specific

Meaning

combinators

Value

Type Class resolution

Type-Level DSLs are

extensible

example

Servant

(haskell)

https://haskell-servant.github.io/

Example: Servant

type HackageAPI =� -- GET /user� "user" :> Get '[JSON] [UserSummary]� -- GET /user/:username� :<|> "user" :> Capture "username" Username :> Get '[JSON] UserDetailed� :<|> "packages" :> Get '[JSON] [Package]

Type Class resolution

(value)

Haskell Client

(value)

Web Server

(value)

Mock Server

let’s build a Type-Level DSL

together

The Problem: Heterogeneous Event Sink

“data lake”

The Problem: Heterogeneous Event Sink

{ “name”: “click”,� “payload”: { ... }�}

{ “name”: “play”,� “payload”: { ... }�}

{ “name”: “pause”,� “payload”: { ... }�}

{ “name”: “click”,

“payload”: {

“user”: “lambda”,� “page:” “track/world”

}

}

{ “name”: “play”,

“payload”: {

“user”: “lambda”,� “track:” 420

}

}

The Problem: Heterogeneous Event Sink

Our Event Sink must:

1. Accept events of different types
2. Dispatch on event name
3. Parse payload into a type depending on the name

Our Type-Level DSL: Three Steps

Haskell

type Events = � ( Click, � ( Play, � ( Pause,� EndOfList) ) )

​

Scala

type Events = � ( Click,� ( Play, � ( Pause,� EndOfList) ) )

1. Encoding lists of types as embedded tuples
2. A typeclass to interpret Events and generate the value “click, play, pause”
3. A handleEvent method using a typeclass to dispatch and parse an event.

Encoding Lists of Types as Embedded Tuples

type EndOfList = Unit

[Int, String, Char] → (Int, (String, (Char, EndOfList))))

let’s begin!

source: http://jjjjjjjjjjohn.tumblr.com/

goo.gl/em6KpH

A little bit about typeclass induction

induction: base case

​

​

implicit val baseCaseName = new Named[EndOfList] { � val name = “”�}

induction step

type Events = (Click, (Play, (Pause, EndOfList)))�type Events = (� (Click, Named[(Click, (Play, (Pause, EndOfList)))]�

(Play, Named[(Play,(Pause, EndOfList))]�

(Pause, Named[(Pause, EndOfList)]�

EndOfList))) Named[EndOfList]

implicit val

implicit def

implicit def

implicit def

dynamic dispatch,

statically!

Recap: interpreter #1

type Events = (Click, (Play, (Pause, EndOfList)))��trait Named[E] { val name: String }�implicit val namedClick: Named[Click]�implicit val namedPlay: Named[Play]�implicit val namedPause: Named[Pause]�implicit val namedBaseCase: Named[EndOfList]�implicit def induction[E](implicit t: Named[Tail]): Named[(E,Tail)]

$ getNamed[Events] = “click, play, pause,”

Recap: interpreter #2

type Events = (Click, (Play, (Pause, EndOfList)))��trait HandleEvents[E] {� type Out� def handleEvent(s: String, String): Either[String, Out] �}�implicit def induction[E](implicit n: Named[E], f: FromString[E], t: HandleEvents[Tail]): HandleEvents[(E,Tail)]

$ handleEvent[Events]("play", "lambdaworld\t123") =� “Right(Left(Right(Play(lambdaworld,123))))”

​

can we have it all?

almost?....!

No instance for (FromString Int) arising from a use of ‘handleEvent’

error: could not find implicit value for parameter names:

HandleEvents[Events]

handleEvent :: Handle events => Proxy events -> String -> String -> Out events

handleEvent :: Handle events => String -> String -> Out events

Couldn't match type ‘Out events’ with ‘Out events0’�NB: ‘Out’ is a type function, and may not be injective�The type variable ‘events0’ is ambiguous�Expected type: String -> String -> Out events� Actual type: String -> String -> Out events0�In the ambiguity check for the type signature for ‘handle’:� handle :: forall (k :: BOX) (events :: k).�…….�…….�…….

Dialectics

Dialectics

DSLs

Type-Level DSLs

contradiction

Extensibility

Dialectics

Runtime

Bugs

Compiler

Bugs

❤️

Interpreting Values

​

contradiction?

Recap

• Type-Level DSLs use typeclass resolution to crawl type-level lists and generate values.
• Type-Level DSLs are extensible
• Type-Level DSLs use core language constructs
• Type-Level DSLs availalbe in Scala *and* Haskell
• Type-Level DSLs are found in the wild: Servant (haskell), Shapeless (scala)
• But compiler errors can be unforgiving
• Until we have Idris, Type-Level DSLs are our only hope!

thank you

(everything after this slide are rejected slides)

❤️ Values

Dialectics

Object

Function

???

contradiction

Dialectics

Type-Level DSL

Value

Domain-Specific

Meaning

combinators

???

compiler

induction

be like