Derived form for datatypes

Makefile

@@ -4,8 +4,8 @@
 
 NAME = 1ml
 MODULES = \
-  lib source prim syntax parser lexer \
-  fomega types iL env erase trace sub import elab \
+  lib source prim fomega types env syntax \
+  parser lexer iL erase trace sub import elab \
   lambda compile \
   main
 NOMLI = syntax iL main import

elab.ml

@@ -610,6 +610,7 @@ Trace.debug (lazy ("[RecT] t = " ^ string_of_norm_typ t));
       ExT([], t), Pure, lift_warn exp.at t env (zs1 @ zs2 @ zs3),
       IL.LetE(e, "_", materialize_typ t)
     )
+
   | EL.ImportE(path) ->
     (match Import.resolve (Source.at_file path) path.it with
     | None -> Source.error path.at ("\""^path.it^"\" does not resolve to a file")
@@ -624,6 +625,9 @@ Trace.debug (lazy ("[RecT] t = " ^ string_of_norm_typ t));
     in
     elab_exp env exp l
 
+  | EL.WithEnvE (toExp) ->
+    elab_exp env (toExp env) l
+
 (*
 rec (X : (b : type) => {type t; type u a}) fun (b : type) => {type t = (X int.u b, X bool.t); type u a = (a, X b.t)}
 s1 = ?Xt:*->*, Xu:*->*->*. !b:*. [= b] -> {t : [= Xt b], u : !a:*. [= a] => [= Xu b a]}

examples/fc.1ml

@@ -9,26 +9,14 @@ local import "prelude"
 ;; clarity.
 
 GADTs = {
-  Exp = {
-    local
-      type I (type t _) = {
-        type case _
-        Zero       :               case int
-        Succ       :      t int ~> case int
-        Pair 'a 'b : t a ~> t b ~> case (a, b)
-      }
-      ...rec {type t _} => {type t a = wrap (m: I t) ~> m.case a}
-      I = I t
-    t
-    case (m: I) (e: t _) = e m
-    Zero     : t _ = fun (m: I) => m.Zero
-    Succ x   : t _ = fun (m: I) => m.Succ x
-    Pair l r : t _ = fun (m: I) => m.Pair l r
+  Exp = data case t _ :> {
+    Zero       :               case int
+    Succ       :      t int ~> case int
+    Pair 'a 'b : t a ~> t b ~> case (a, b)
   }
 
   eval = rec (eval 'a: Exp.t a ~> a) =>
-    Exp.case {
-      type case x = x
+    Exp.case (type fun x => x) {
       Zero = 0
       Succ x = eval x + 1
       Pair l r = (eval l, eval r)

examples/hoas.1ml

@@ -5,35 +5,13 @@ local import "prelude"
 ;;
 ;;   https://github.com/palladin/idris-snippets/blob/master/src/HOAS.idr
 
-let
-  type I (type case _) (type t _) = {
-    Val 'x       :                           x ~> case x
-    Bin 'x 'y 'z : (x ~> y ~> z) ~> t x ~> t y ~> case z
-    If  'x       :      t Bool.t ~> t x ~> t x ~> case x
-    App 'x 'y    :           t (x ~> y) ~> t x ~> case y
-    Lam 'x 'y    :                (t x ~> t y) ~> case (x ~> y)
-    Fix 'x 'y    :      t ((x ~> y) ~> x ~> y) ~> case (x ~> y)
-  }
-  type J (type t _) = {type case _, ...I case t}
-  type T (type t _) x = (c: J t) ~> c.case x
-  ...{
-    ...rec {type t _} => {type t x = wrap T t x}
-    case 'x (type case _) (cs: I case t) (e: t _) = e {case, ...cs}
-    mk (fn: T t _) = fn
-  } :> {
-    type t _
-    case 'x: (type case _) -> I case t -> t x ~> case x
-    mk 'x: T t x -> t x
-  }
-  J = J t
-in {
-  t, case
-  Val 'x                                   (v: x) = mk fun (e: J) => e.Val v
-  Bin 'x 'y 'z (f: x ~> y ~> z) (l: t x) (r: t y) = mk fun (e: J) => e.Bin f l r
-  If  'x          (b: t Bool.t) (c: t x) (a: t x) = mk fun (e: J) => e.If b c a
-  App 'x 'y              (f: t (x ~> y)) (a: t x) = mk fun (e: J) => e.App f a
-  Lam 'x 'y                       (f: t x ~> t y) = mk fun (e: J) => e.Lam f
-  Fix 'x 'y           (f: t ((x ~> y) ~> x ~> y)) = mk fun (e: J) => e.Fix f
+data case t _ :> {
+  Val 'x       :                           x ~> case x
+  Bin 'x 'y 'z : (x ~> y ~> z) ~> t x ~> t y ~> case z
+  If  'x       :      t Bool.t ~> t x ~> t x ~> case x
+  App 'x 'y    :           t (x ~> y) ~> t x ~> case y
+  Lam 'x 'y    :                (t x ~> t y) ~> case (x ~> y)
+  Fix 'x 'y    :      t ((x ~> y) ~> x ~> y) ~> case (x ~> y)
 }
 
 Fact = Fix <| Lam fun f => Lam fun x =>

examples/tiv.1ml

@@ -0,0 +1,116 @@
+local import "prelude"
+
+;; As 1ML is powerful enough to encode GADTs we can define a value independent
+;; type representation or a deep embedding of type constructors.
+
+type iso a b = {to: a ~> b, from: b ~> a}
+
+Rep = {
+  data case t _ :> {
+    bool: case bool
+    char: case char
+    int : case int
+    text: case text
+    unit: case unit
+
+    alt  'x 'y: t x ~> t y ~> case (alt x y)
+    ~~>  'x 'y: t x ~> t y ~> case (x ~> y)
+    pair 'x 'y: t x ~> t y ~> case (x, y)
+
+    iso 'x 'y: iso x y ~> t y ~> case x
+
+    lazy 'x: ({} ~> t x) ~> case x
+  }
+
+  defaults (type t _) (default 'a: t a) = {
+    bool = default
+    char = default
+    int  = default
+    unit = default
+    text = default
+
+    alt   _ _ = default
+    _ ~~> _   = default
+    pair  _ _ = default
+
+    iso _ _ = default
+
+    lazy _ = default
+  }
+
+  local i = {to = Opt.case {none = inl {}, some = inr}
+             from = Alt.case {inl {} = none, inr = some}}
+  opt a = iso i (alt unit a)
+
+  local i = {to = List.case {nil = inl {}, x :: xs = inr (x, xs)}
+             from = Alt.case {inl {} = nil, inr (x, xs) = x::xs}}
+  list v = rec vs => lazy fun {} => iso i (alt unit (pair v vs))
+}
+
+;; Generic toText
+
+ToText = {type t x = x ~> text}
+
+toText = rec (toText 'x: Rep.t x ~> ToText.t x) => Rep.case ToText.t {
+  bool = Bool.toText
+  char c =  "'" ++ Text.fromChar c ++ "'"
+  int = Int.toText
+  text t = "\"" ++ t ++ "\""
+  unit {} = "{}"
+
+  alt aT bT = Alt.case {
+    inl a = "(inl " ++ toText aT a ++ ")"
+    inr b = "(inr " ++ toText bT b ++ ")"
+  }
+
+  (_ ~~> _) _ = "<fun>"
+
+  pair aT bT (a, b) = "(" ++ toText aT a ++ ", " ++ toText bT b ++ ")"
+
+  iso ab bT = ab.to >> toText bT
+
+  lazy th = toText (th {})
+}
+
+println rep x = print (toText rep x ++ "\n")
+
+do let ...Rep
+   println int 101
+   println (pair bool text) (true, "that")
+   println (opt bool) (some false)
+   println (iso {to i = i <> 0, from b = if b then 1 else 0} bool) 1
+   println (list int) (3 :: (1 :: (4 :: nil)))
+
+;; Generic eq
+
+Eq = {type t x = x ~> x ~> bool}
+
+eq = rec (eq 'x: Rep.t x ~> Eq.t x) => Rep.case Eq.t {
+  bool = Bool.==
+  char = Char.==
+  int = Int.==
+  text = Text.==
+  unit _ _ = true
+
+  alt aT bT l r = l |> Alt.case {
+    inl l = r |> Alt.case {inl = eq aT l, inr _ = false}
+    inr l = r |> Alt.case {inl _ = false, inr = eq bT l}
+  }
+
+  (_ ~~> _) _ _ = false
+
+  pair aT bT (l1, l2) (r1, r2) = eq aT l1 r1 && eq bT l2 r2
+
+  iso ab bT l r = eq bT (ab.to l) (ab.to r)
+
+  lazy th l r = eq (th {}) l r
+}
+
+do let ...Rep
+       test t l r = print ("eq " ++ toText t l ++
+                             " " ++ toText t r ++
+                           " = " ++ toText bool (eq t l r) ++ "\n")
+   test int 101 42
+   test (pair int bool) (1, true) (1, true)
+   test (list int) (3 :: (1 :: nil)) (4 :: (1 :: nil))
+   test (list int) (4 :: (2 :: nil)) (4 :: (2 :: nil))

examples/trie.1ml

@@ -1,25 +1,14 @@
 local import "prelude"
 
 FunctionalTrie = {
-  local
-    type I (type t _ _) = {
-      type case _ _
-      unit 'v         : opt v            ~> case {} v
-      alt  'v 'k1 'k2 : t k1 v ~> t k2 v ~> case (alt k1 k2) v
-      pair 'v 'k1 'k2 : t k1 (t k2 v)    ~> case (k1, k2) v
-    }
-    ...rec {type t _ _} => {type t k v = wrap (m: I t) ~> m.case k v}
-    I = I t
-
-  t
-  case (m: I) (e: t _ _) = e m
-  unit vO : t _ _ = fun (m: I) => m.unit vO
-  alt l r : t _ _ = fun (m: I) => m.alt l r
-  pair lr : t _ _ = fun (m: I) => m.pair lr
+  data case t _ _ :> {
+    unit 'v         : opt v            ~> case {} v
+    alt  'v 'k1 'k2 : t k1 v ~> t k2 v ~> case (alt k1 k2) v
+    pair 'v 'k1 'k2 : t k1 (t k2 v)    ~> case (k1, k2) v
+  }
 
   lookup = rec (lookup 'k 'v: t k v ~> k ~> opt v) =>
-    case {
-      type case k v = k ~> opt v
+    case (type fun k v => k ~> opt v) {
       unit m {} = m
       alt ta tb = Alt.case {inl = lookup ta, inr = lookup tb}
       pair ta (a, b) = lookup ta a |> Opt.case {none, some tb = lookup tb b}

lexer.mll

@@ -263,6 +263,7 @@ rule token = parse
   | "_" { HOLE }
   | "&&" { LOGICAL_AND }
   | "as" { AS }
+  | "data" { DATA }
   | "do" { DO }
   | "else" { ELSE }
   | "type_check" { TYPE_CHECK }

parser.mly

@@ -39,6 +39,7 @@ let parse_error s = raise (Source.Error (Source.nowhere_region, s))
 %token IMPORT
 %token WRAP_OP UNWRAP_OP
 %token ROLL_OP UNROLL_OP
+%token DATA
 
 %token EOF
 
@@ -424,6 +425,8 @@ annexp :
     { $2($1, $3)@@at() }
 ;
 exp :
+  | DATA name name typparamlist annexp_op typ
+    { dataE($2, $3, $4, $5, $6, at())@@at() }
   | LET bind IN exp
     { letE($2, $4)@@at() }
   | IF exp THEN exp ELSE exp
@@ -506,6 +509,8 @@ atbind :
     { inclB(letE($2, $4)@@at())@@at() }
   | IMPORT TEXT
     { InclB(ImportE($2@@ati 2)@@at())@@at() }
+  | DATA name name typparamlist annexp_op typ
+    { InclB(dataE($2, $3, $4, $5, $6, at())@@at())@@at() }
 /*
   | LPAR bind RPAR
     { $2 }

prelude/index.1mls

@@ -83,6 +83,10 @@ Text: {
   print: t ~> {}
 }
 
+Unit: {
+  type t = {}
+}
+
 Zero: {
   type t
 }
@@ -94,6 +98,7 @@ type int = Int.t
 type list a = List.t a
 type opt a = Opt.t a
 type text = Text.t
+type unit = Unit.t
 type zero = Zero.t
 
 % * + - / : int -> int -> int