gdritter repos documents / 9f70639
Some typed latka syntax changes Getty Ritter 9 years ago
1 changed file(s) with 19 addition(s) and 20 deletion(s). Collapse all Expand all
+19
-20
scraps/typed-latka.md less more
77 puts syll (rep.6.syll)
88
99 (* We can now define rep in-language as
10 * rep (fixed n : Nat) (s : String) : String =
11 case n of
12 0 . ""
13 1 . s
14 _ . s (rep.(pred.n).s)
15 *)
10
11 rep : Num -> String -> String
12 !0 _ = ""
13 !1 s = s
14 !n s = s rep.(pred.n).s
15 *)
1616
1717 (* It is acceptable that all arguments must be explicitly specified. *)
1818
19 fact (fixed n : Nat) : Nat=
20 case n of
21 0 . 0
22 _ . mul.n.(fact.(pred.n))
19 fact : Num -> Num
20 !0 = 0
21 !n = mul.n.(fact.(pred.n))
2322
2423 (* We have both labeled sums and records, where the records are closer to
2524 * the ML style than the Haskell style. `alias` is Haskell's `type` *)
2625
27 alias Person =
28 { name : String
29 , age : Nat
26 type Person =
27 { .name String
28 , .age Nat
3029 }
3130
32 data Character =
33 Character Person
31 type Character = [ Character Person ]
3432
3533 (* Type variables work as in Haskell *)
3634
37 data List a = Nil | Cons a (List a)
35 type List a = [ Nil
36 | Cons a (List a)
37 ]
3838
39 map (f : a -> b) (ls : List a) =
40 case ls of
41 Cons x xs . Cons.(f.x).xs
42 _ . Nil
39 map : (a -> b) -> List a -> List b
40 !f !(Cons x xs) = Cons.(f.x).(map.f.xs)
41 !f !Nil = Nil
4342
4443 (* We can explicitly indicate a subtyping (convertibility)
4544 * relationship, so long as our conv instances form a DAG. *)