LambdAle code talk. A love letter to Idris and its perhaps-too-bendy syntax.

Talk.idr

module Talk

-- Tom Harding
--
-- Blog:    tomharding.me
-- GitHub:  github.com/i-am-tom
-- Twitter: twitter.com/am_i_tom
-- Work:    habito.com

-- github.com/i-am-tom/LICK

import Data.List
import Data.HVect

%language DSLNotation


-------------------------------------------------------------------------------
-- 1. Dependent types.

typeOf : (a : t) -> Type
typeOf {t} _ = t

the : (a : Type) -> a -> a
the _ = id


-------------------------------------------------------------------------------
-- 2. Untyped λ-calculus.

data UTLC
  = UVar String
  | UAbs String UTLC
  | UApp UTLC UTLC


-------------------------------------------------------------------------------
-- 3. UTλC interpreter.

evaluateU : UTLC -> Maybe ?idk
--                  ^^^^^ ^^^^
evaluateU = ?idc


-------------------------------------------------------------------------------
-- 4. Simply-typed λ-calculus.

infixr 10 :->:

data SType
  = SString | SInt | SBool
  | (:->:) SType SType

data STLC
  = SVar String
  | SAbs String SType STLC
  | SApp STLC STLC


-------------------------------------------------------------------------------
-- 5. STλC interpreter.

evaluateS : STLC -> Maybe ?idk
evaluateS = ?idc


-------------------------------------------------------------------------------
-- 6. Type, define, refine.

data STLC' : (result : SType) -> Type where
  SAbs'
     : String
    -> (input : SType)
    -> STLC' output
    -> STLC' (input :->: output)

  SApp'
     : STLC' (input :->: output)
    -> STLC' input
    -> STLC' output

  SVar'
     : String
    -> STLC' ?huh


-------------------------------------------------------------------------------
-- 7. The 'Elem' type.

data Elem' : a -> List a -> Type where
  Here'  : Elem' x (x :: xs)
  There' : Elem' x xs -> Elem' x (y :: xs)


-------------------------------------------------------------------------------
-- 8. More typed, more defined, more refined.

data STLC'' : (context : List SType) -> (result : SType) -> Type where
  SAbs''
     : {input : SType}
    -> STLC'' (input :: context) output
    -> STLC'' context (input :->: output)

  SApp''
     : STLC'' context (input :->: output)
    -> STLC'' context input
    -> STLC'' context output

  SVar''
     : Elem reference context
    -> STLC'' context reference


-------------------------------------------------------------------------------
-- 9. Back to normal types.

STypeToType : SType -> Type
STypeToType SString    = String
STypeToType SInt       = Int
STypeToType SBool      = Bool
STypeToType (a :->: b) = STypeToType a -> STypeToType b


-------------------------------------------------------------------------------
-- 10. Build a context.

ContextToVect : (input : List SType) -> Vect (length input) Type
ContextToVect []        = []
ContextToVect (x :: xs) = STypeToType x :: ContextToVect xs


-------------------------------------------------------------------------------
-- 11. Get a value.

get
   : List.Elem ref sTypes
  -> HVect (ContextToVect sTypes)
  -> STypeToType ref

get Here (head :: _)
  = head

get (There later) (_ :: tail)
  = get later tail


-------------------------------------------------------------------------------
-- 12. Evaluation.

evaluate
   : {context : List SType}
  -> HVect (ContextToVect context)
  -> STLC'' context result
  -> STypeToType result

evaluate context (SAbs'' f)
  = \input => evaluate (input :: context) f

evaluate context (SApp'' f x)
  = (evaluate context f)
    (evaluate context x)

evaluate context (SVar'' ref)
  = get ref context


-------------------------------------------------------------------------------
-- 13. Syntax.

dsl stlc
    variable    = SVar''
    lambda      = const SAbs''
    index_first = Here
    index_next  = There


-------------------------------------------------------------------------------
-- 14. Overloading.

(<*>) : STLC'' ctx (a :->: b) -> STLC'' ctx a -> STLC'' ctx b
(<*>) = SApp''

pure : STLC'' ctx a -> STLC'' ctx a
pure = id


-------------------------------------------------------------------------------
-- 15. Code in code.

id : STLC'' ctx (a :->: a)
id = stlc (\x => x)

const : STLC'' ctx (a :->: b :->: a)
const = stlc (\x => \_ => x)

flip : STLC'' ctx ((a :->: b :->: c) :->: (b :->: a :->: c))
flip = stlc (\f => \x => \y => [| f y x |])


-------------------------------------------------------------------------------
-- 16. "Types vs tests" vs "Types for tests".

test : evaluate {context = []} [] (id {a = SInt}) 2 = 2
test = Refl