180 lines
2.9 KiB
Plaintext
180 lines
2.9 KiB
Plaintext
{# type Type #} ,
|
|
|
|
{# class Class #} ,
|
|
|
|
-- Classes
|
|
|
|
Semigroup : Type -> Class,
|
|
Semigroup = a -> {{
|
|
append : a -> a -> a
|
|
}},
|
|
|
|
Monoid : Type -> Class,
|
|
Monoid = a -> {{
|
|
semigroup : {{ Semigroup a }},
|
|
empty : a
|
|
}},
|
|
|
|
-- Types
|
|
|
|
Void : Type,
|
|
Void = {
|
|
Void : Type,
|
|
Void = a,
|
|
|
|
semigroup : {{ Semigroup Void }},
|
|
semigroup = {{
|
|
append = []
|
|
}},
|
|
},
|
|
|
|
Unit : Type,
|
|
Unit = {
|
|
Unit : Type,
|
|
Unit = {},
|
|
|
|
semigroup : {{ Semigroup Unit }},
|
|
semigroup = {{
|
|
append = _ _ -> {},
|
|
}},
|
|
|
|
monoid : {{ Monoid Unit }},
|
|
monoid = {{
|
|
empty = {},
|
|
}},
|
|
},
|
|
|
|
|
|
{# prim bool Bool #},
|
|
Bool : Type,
|
|
Bool = {
|
|
Bool : Type,
|
|
Bool = [false : {}, true : {}],
|
|
|
|
Any : Type,
|
|
Any = {
|
|
semigroup : {{ Semigroup Bool }},
|
|
semigroup = {{
|
|
append = a -> [false = a, true = true],
|
|
}},
|
|
|
|
monoid : {{ Monoid Bool }},
|
|
monoid = {{ empty = false }},
|
|
},
|
|
|
|
All : Type,
|
|
All = {
|
|
semigroup : {{ Semigroup Bool }},
|
|
semigroup = {{
|
|
append = a -> [false = false, true = a],
|
|
}},
|
|
|
|
monoid : {{ Monoid Bool }},
|
|
monoid = {{ empty = true }},
|
|
},
|
|
},
|
|
|
|
|
|
Int : Type,
|
|
Int = {
|
|
{# prim i64 Int #},
|
|
Int : Type,
|
|
Int = [zero : {}, succ : Nat ],
|
|
|
|
Additive : Type,
|
|
Additive = {
|
|
semigroup : {{ Semigroup Int }},
|
|
semigroup = {{
|
|
append = n -> [zero = n, succ = m -> succ (append n m) ],
|
|
}},
|
|
|
|
monoid : {{ Monoid Int }},
|
|
monoid = {{
|
|
empty = zero,
|
|
}},
|
|
},
|
|
|
|
Multiplicative : Type,
|
|
Multiplicative = {
|
|
semigroup : {{ Semigroup Int }},
|
|
semigroup = {{
|
|
append = n -> [zero = zero, succ = m -> Additive.append n (append n m) ],
|
|
}},
|
|
|
|
monoid : {{ Monoid Int }},
|
|
monoid = {{
|
|
empty = succ zero,
|
|
}},
|
|
},
|
|
},
|
|
|
|
Pair : Type,
|
|
Pair = {
|
|
Pair : Type -> Type -> Type,
|
|
Pair = a -> b -> { left : a, right : b },
|
|
|
|
semigroup : {{ Semigroup A }} -> {{ Semigroup B }} -> {{ Semigroup (Pair A B) }},
|
|
semigroup = {{
|
|
append = { a0, b0 } { a1, b1 } -> { append a0 a1, append b0 b1 }
|
|
}},
|
|
|
|
monoid : {{ Monoid A }} -> {{ Monoid B }} -> {{ Monoid (Pair A B) }},
|
|
monoid = {{
|
|
empty = { empty, empty },
|
|
}},
|
|
},
|
|
|
|
Either : Type,
|
|
Either = {
|
|
Either : Type -> Type -> Type,
|
|
Either = a b -> [ left : a, right : b ],
|
|
|
|
Left : Type,
|
|
Left = {
|
|
semigroup : {{ Semigroup (Either A B) }},
|
|
semigroup = {{
|
|
append = l _ -> l,
|
|
}},
|
|
},
|
|
|
|
Right : Type,
|
|
Right = {
|
|
semigroup : {{ Semigroup (Either A B) }},
|
|
semigroup = {{
|
|
append = _ r -> r
|
|
}},
|
|
},
|
|
},
|
|
|
|
List : Type,
|
|
List = {
|
|
List : Type -> Type,
|
|
List = a -> [ nil : {} , cons : { head : A , tail : List a } ],
|
|
|
|
semigroup : {{ Semigroup (List a) }},
|
|
semigroup = {{
|
|
append = [
|
|
nil = {} -> b -> b,
|
|
cons = {a, as} -> b -> cons a (append as b),
|
|
],
|
|
}},
|
|
|
|
monoid : {{ Monoid (List a) }},
|
|
monoid = {{
|
|
empty = nil,
|
|
}},
|
|
},
|
|
|
|
{# prim char Char #},
|
|
Char : Type,
|
|
|
|
{# prim string String #},
|
|
String : Type,
|
|
String = List Char,
|
|
|
|
{# builtin show Show #},
|
|
Show : Type -> Class,
|
|
Show = a -> {{
|
|
show : a -> String,
|
|
}},
|