From 5047ecf6db8c96aab52da3cedcbeaed63fafd56e Mon Sep 17 00:00:00 2001 From: Vesa Karvonen Date: Tue, 23 Jun 2020 07:22:59 +0300 Subject: [PATCH] Add syntax for annotating the result of type binds, pats, and decs Type bindings, patterns, and declarations assume that the result is `type`. For example, the declaration type t x is equivalent to t: type -> type This commit allows the type to be specified explicitly using an optional annotation. Both type t x: type and type t: type -> type are equivalent to the previous two definitions. --- examples/type-level.1ml | 135 ++++++++++++++++++++++++++++++---------- parser.mly | 51 +++++++++------ regression.1ml | 16 +++++ 3 files changed, 151 insertions(+), 51 deletions(-) diff --git a/examples/type-level.1ml b/examples/type-level.1ml index 28fdba0b..6abe3fa8 100644 --- a/examples/type-level.1ml +++ b/examples/type-level.1ml @@ -2,74 +2,143 @@ local import "prelude" ;; 1ML basically gives you simply typed lambda calculus (STLC) at the type ;; level, which is unsurprising as 1ML is just as powerful as Fω. You can even -;; use lambda and let -expressions at the type level (note the `fst` and `snd` -;; definitions below). So, you can encode various kinds of stuff at the type -;; level. Of course, STLC is quite restrictive. +;; use lambda and let -expressions at the type level. STLC is quite +;; restrictive, but you can still encode various kinds of stuff at the type +;; level. -TypeLevel = { +TypeLevel: { + Pair: { + type t = (type _ _ _) -> type + + fst: t -> type + snd: t -> type + + of: type -> type -> t + + cross: (type _ _) -> (type _ _) -> t -> t + + map: (type _ _) -> t -> t + } + + Bool: { + type t = type -> type -> type + + true: t + false: t + + not: t -> t + + andAlso: t -> t -> t + orElse: t -> t -> t + + equals: t -> t -> t + } + + Alt: { + type t = (type _ _) -> (type _ _) -> type + + inL: type -> t + inR: type -> t + + isL: t -> Bool.t + isR: t -> Bool.t + + case: t -> t + } + + Nat: { + type t = (type _ _) -> type -> type + + isZero: t -> Bool.t + + zero: t + one: t + + succ: t -> t + (+): t -> t -> t + (*): t -> t -> t + } + + List: { + type t = type -> (type _ _ _) -> type + + nil: t + (::): type -> t -> t + + map: (type _ _) -> t -> t + + isNil: t -> Bool.t + + head: t -> type + } +} = { Pair = { type t = (type _ _ _) -> type - type fst (p: t) = p fun fst _ => fst - type snd (p: t) = p fun _ snd => snd + type fst (p: t): type = p fun fst _ => fst + type snd (p: t): type = p fun _ snd => snd - type of fst snd (type d _ _) = d fst snd + type of fst snd: t = fun (type d _ _) => d fst snd - type cross (type f _) (type s _) (p: t) (type d _ _) = + type cross (type f _) (type s _) (p: t): t = fun (type d _ _) => of (f (fst p)) (s (snd p)) d - type map (type f _) (p: t) (type d _ _) = cross f f p d + type map (type f _) (p: t): t = fun (type d _ _) => cross f f p d } Bool = { type t = type -> type -> type - type true true _ = true - type false _ false = false + type true: t = fun true _ => true + type false: t = fun _ false => false - type not (x: t) true false = x false true + type not (x: t): t = fun true false => x false true - type andAlso (l: t) (r: t) false true = l (r true false) false - type orElse (l: t) (r: t) false true = l true (r true false) + type andAlso (l: t) (r: t): t = fun false true => l (r true false) false + type orElse (l: t) (r: t): t = fun false true => l true (r true false) - type equals (l: t) (r: t) true false = l (r true false) (r false true) + type equals (l: t) (r: t): t = + fun true false => l (r true false) (r false true) } Alt = { - type t = (type -> type) -> (type -> type) -> type + type t = (type _ _) -> (type _ _) -> type - type inL v (type inL _) (type _ _) = inL v - type inR v (type _ _) (type inR _) = inR v + type inL v: t = fun (type inL _) (type _ _) => inL v + type inR v: t = fun (type _ _) (type inR _) => inR v - type isL (a: t) true false = a (fun _ => true) (fun _ => false) - type isR (a: t) true false = a (fun _ => false) (fun _ => true) + type isL (a: t): Bool.t = + fun true false => a (fun _ => true) (fun _ => false) + type isR (a: t): Bool.t = + fun true false => a (fun _ => false) (fun _ => true) type case (a: t) (type inL _) (type inR _) = a inL inR } Nat = { - type t = (type -> type) -> type -> type + type t = (type _ _) -> type -> type - type isZero (n: t) true false = n (fun _ => false) true + type isZero (n: t): Bool.t = fun true false => n (fun _ => false) true - type zero (type _ _) zero = zero - type one (type succ _) zero = succ zero + type zero: t = fun (type _ _) zero => zero + type one: t = fun (type succ _) zero => succ zero - type succ (n: t) (type succ _) zero = succ (n succ zero) - type plus (m: t) (n: t) (type succ _) zero = n succ (m succ zero) - type times (m: t) (n: t) (type succ _) zero = n (m succ) zero + type succ (n: t): t = fun (type succ _) zero => succ (n succ zero) + type (m: t) + (n: t): t = fun (type succ _) zero => n succ (m succ zero) + type (m: t) * (n: t): t = fun (type succ _) zero => n (m succ) zero } List = { - type t = type -> (type -> type -> type) -> type + type t = type -> (type _ _ _) -> type - type nil nil (type _ :: _) = nil - type (x :: (xs: t)) nil (type _ :: _) = x :: xs nil (::) + type nil : t = fun nil (type _ :: _) => nil + type (x :: (xs: t)): t = fun nil (type _ :: _) => x :: xs nil (::) - type map (type fn _) (xs: t) nil (type _ :: _) = xs nil fun x => (::) (fn x) + type map (type fn _) (xs: t): t = + fun nil (type _ :: _) => xs nil fun x => (::) (fn x) - type isNil (xs: t) true false = xs true fun _ _ => false + type isNil (xs: t): Bool.t = fun true false => xs true fun _ _ => false - type head (xs: t) = xs zero fun h _ => h + type head (xs: t): type = xs zero fun h _ => h } } diff --git a/parser.mly b/parser.mly index a6c9bf5b..918cb198 100644 --- a/parser.mly +++ b/parser.mly @@ -116,10 +116,12 @@ implparam : annparam : | LPAR head COLON typ RPAR { (headB($2)@@ati 2, $4, Expl@@ati 3)@@at() } - | LPAR typpat RPAR - { let (head, typparams) = $2 in - (headB(head)@@head.at, funT(typparams, TypT@@at(), Pure@@ati 2)@@ati 2, - Expl@@ati 2)@@at() } + | LPAR typpat optannot RPAR + { let (h, tps) = $2 in + (headB(h)@@h.at, + funT(tps, + Lib.Option.value $3 ~default:(TypT@@at()), Pure@@ati 2)@@ati 2, + Expl@@ati 2)@@at() } | implparam { $1 } ; @@ -220,9 +222,9 @@ optannot : opttypdef : | - { TypT@@at() } + { None } | EQUAL typ - { EqT(typE($2)@@ati 2)@@ati 2 } + { Some (typE($2)@@ati 2) } ; atdec : @@ -233,8 +235,16 @@ atdec : @@at() } | name { VarD($1, funT([], EqT(VarE($1)@@ati 1)@@ati 1, Pure@@ati 1)@@ati 1)@@at() } - | typdec opttypdef - { VarD(fst $1, funT(snd $1, $2, Pure@@at())@@at())@@at() } + | typdec optannot opttypdef + { VarD(fst $1, + funT(snd $1, + (match $2, $3 with + | None, None -> TypT@@at() + | Some t2, None -> t2 + | None, Some te3 -> EqT(te3)@@ati 3 + | Some t2, Some te3 -> + EqT(annotE(te3, t2)@@span[ati 2; ati 3])@@span[ati 2; ati 3]), + Pure@@at())@@at())@@at() } | ELLIPSIS typ { InclD($2)@@at() } | LET bind IN typ @@ -431,8 +441,8 @@ atbind : { patB($1, $2($4))@@at() } | name { VarB($1, VarE($1.it@@at())@@at())@@at() } - | typpat EQUAL typ - { VarB(fst $1, funE(snd $1, typE($3)@@ati 3)@@at())@@at() } + | typpat bindanns_opt EQUAL typ + { VarB(fst $1, funE(snd $1, $2(typE($4)@@span[ati 2; ati 4]))@@at())@@at() } | ELLIPSIS exp { InclB($2)@@at() } | DO exp @@ -470,10 +480,12 @@ atpat : { annotP(headP($2)@@$2.at, funT($3::$4, $6, Pure@@at())@@at())@@at() } | LPAR patlist RPAR { match $2 with [p] -> p | ps -> tupP(ps, at())@@at() } - | LPAR typpat RPAR - { let (head, typparams) = $2 in - annotP(headP(head)@@head.at, - funT(typparams, TypT@@at(), Pure@@at())@@at())@@at() } + | LPAR typpat optannot RPAR + { let (h, tps) = $2 in + annotP(headP(h)@@h.at, + funT(tps, + Lib.Option.value $3 ~default:(TypT@@at()), + Pure@@at())@@at())@@at() } ; annpat_op : | COLON @@ -510,10 +522,13 @@ atdecon : | name typparam typparamlist COLON typ { ($1, annotP(varP($1)@@$1.at, funT($2::$3, $5, Pure@@at())@@at())@@at())@@at() } - | typdec - { let (name, typparams) = $1 in - (name, annotP(varP(name)@@name.at, - funT(typparams, TypT@@at(), Pure@@at())@@at())@@at())@@at() } + | typdec optannot + { let (n, tps) = $1 in + (n, + annotP(varP(n)@@n.at, + funT(tps, + Lib.Option.value $2 ~default:(TypT@@at()), + Pure@@at())@@at())@@at())@@at() } /* | LPAR decon RPAR { $2 } diff --git a/regression.1ml b/regression.1ml index e871ebfb..66b1adeb 100644 --- a/regression.1ml +++ b/regression.1ml @@ -74,6 +74,22 @@ do ManifestTycon.t {} {type t = int, x = 1} ;; +Nat: { + type t = (type _ _ : type) -> type -> type + type Zero : t = fun (type S _ : type) Z : type => Z + type Inc (n: t) : t = fun (type S _ : type) Z : type => S (n S Z) +} = {} + +let + {type P _: type -> type} = {P = Pair.t} + (type P' _: type -> type) = Pair.t + F (type P _: type -> type) = P int text + do (42, "101"): F P + do (42, "101"): F P' +in {} + +;; + AmateurOptics = { type FUNCTOR = { type t a