WIP Add 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