178 lines
2.8 KiB
Plaintext
178 lines
2.8 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 = []
|
|
|
|
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
|
|
}}
|