165 lines
3.2 KiB
Plaintext
165 lines
3.2 KiB
Plaintext
-- The empty type is the empty alternative.
|
|
Bot : Type
|
|
Bot = []
|
|
|
|
-- The unit type is the empty record.
|
|
Top : Type
|
|
Top = {}
|
|
|
|
t : Top
|
|
-- Names of literals can be inferred.
|
|
t = {} @Top
|
|
t = {}
|
|
|
|
Cop : Type
|
|
Cop = {}
|
|
|
|
c : Cop
|
|
c = {}
|
|
|
|
-- Renaming
|
|
c : Cop
|
|
c = t @Top
|
|
|
|
-- Dropping names
|
|
k : {}
|
|
k : t @_
|
|
|
|
{} : {}
|
|
|
|
Bool : Type
|
|
Bool = [ false , true ]
|
|
|
|
f : Bool
|
|
f = false
|
|
|
|
t : Bool
|
|
t = true
|
|
|
|
-- data Maybe a = Nothing | Just a
|
|
-- data Maybe : Type -> Type where
|
|
-- Nothing : Maybe a
|
|
-- Just : a -> Maybe a
|
|
|
|
Maybe : Type -> Type
|
|
-- Types can be omitted when they can be inferred:
|
|
Maybe A = [ nothing : Maybe A , just A : Maybe A ]
|
|
Maybe A = [ nothing , just A ]
|
|
|
|
n : Maybe A
|
|
n = nothing
|
|
|
|
j : Maybe Top
|
|
j = just {}
|
|
|
|
Either : Type -> Type -> Type
|
|
Either A B = [ left A , right B ]
|
|
|
|
Nat : Type
|
|
Nat = [ zero : Nat , succ : Nat -> Nat ]
|
|
|
|
two : Nat
|
|
two = succ (succ zero)
|
|
|
|
Pair : Type -> Type -> Type
|
|
Pair A B { fst : A , snd : B }
|
|
-- Without naming the projections
|
|
Pair A B = { A , B }
|
|
|
|
p : Pair A B
|
|
p = { }
|
|
|
|
add : N -> N -> N
|
|
add n m {
|
|
n + m
|
|
}
|
|
|
|
mult : N -> N -> N
|
|
mult n m {
|
|
n * m
|
|
}
|
|
|
|
-- Modules are regular records. This is similar to how records work
|
|
-- in Agda. In other words, this module (record) contains two
|
|
-- elements. The elements of the record are themself functions that
|
|
-- can be exposed by "opening" Bin
|
|
|
|
Arith : Type
|
|
Arith = {
|
|
add :
|
|
}
|
|
|
|
Bin : N -> N -> Type
|
|
Bin n m =
|
|
add : N
|
|
add = n + m,
|
|
|
|
mult : N
|
|
mult = n * m
|
|
}
|
|
|
|
{} : {}
|
|
[] : []
|
|
|
|
|
|
|
|
-- {} is used to *introduce* records/products
|
|
-- pair.fst is used to eleminate records/producs
|
|
|
|
pr : Pair Top Cop
|
|
pr = { {}, {} }
|
|
pr = { fst = {}, snd = {} }
|
|
|
|
fst : Pair A B -> A
|
|
fst { fst } = fst
|
|
|
|
-- [] is used to eliminate alternatives/sums
|
|
either : (a -> c) -> (b -> c) -> Either a b -> c
|
|
either l r e = [ left a = l a, right b = r b ] e
|
|
-- Syntax for case-statements makes -XLambdaCase redundant.
|
|
either l r = [ left a = l a, right b = r b ]
|
|
-- Tags could in theory be omitted just like they can for {}-intro:
|
|
either l r = [ l, r ]
|
|
-- Perhaps the meaning will be rather difficult to decipher though,
|
|
also it would mean that the order in which summands are defined
|
|
become significant which might not be desirable
|
|
|
|
-- Note the duality:
|
|
{ fst = {}, snd = {} } is an introduction.
|
|
[ left a = l a, right b = r b ] is an elimination.
|
|
|
|
|
|
-- Comments could follow the non-decreasing indentation rule as well.
|
|
So that multi-line comments can use the same syntax as single-line
|
|
comments. Just that the comments on following lines must be
|
|
indented more than where the comment marker is located. In this
|
|
example the comment marker is at column 0.
|
|
|
|
Semigroup : Type -> Class
|
|
semigroup a = {
|
|
append : a -> a -> a
|
|
}
|
|
|
|
Monoid : Type -> Class
|
|
Monoid a = {
|
|
{_ Semigroup a _}, -- Curly braces in type signature signal implicit
|
|
arguments.
|
|
-- Could also be written:
|
|
{_ semigroup : Semigroup a _} -- I.e. the braces extend around the
|
|
field name as well.
|
|
empty : a
|
|
}
|
|
|
|
Functor : (Type -> Type) -> Class
|
|
Functor f = {
|
|
map : (a -> b) -> f a -> f b
|
|
}
|
|
|
|
{ empty = Nothing } : {Semigroup a} -> Monoid (Maybe a)
|
|
{ Nothing } : {Semigroup a} -> Monoid (Maybe a)
|
|
|
|
@{T} : [| T |] -> T
|
|
@[T] : T -> [| T |]
|
|
|
|
T@
|