diff options
Diffstat (limited to 'examples')
| -rw-r--r-- | examples/typetheory/Types.gf | 114 |
1 files changed, 114 insertions, 0 deletions
diff --git a/examples/typetheory/Types.gf b/examples/typetheory/Types.gf new file mode 100644 index 000000000..3a477e437 --- /dev/null +++ b/examples/typetheory/Types.gf @@ -0,0 +1,114 @@ +abstract Types = { + +-- Martin-Löf's set theory 1984 + +-- categories +cat + Set ; + El Set ; + +-- basic forms of sets +data + Plus : Set -> Set -> Set ; + Pi : (A : Set) -> (El A -> Set) -> Set ; + Sigma : (A : Set) -> (El A -> Set) -> Set ; + Falsum : Set ; + Nat : Set ; + Id : (A : Set) -> (a,b : El A) -> Set ; + +-- defined forms of sets +fun Impl : Set -> Set -> Set ; +def Impl A B = Pi A (\x -> B) ; + +fun Conj : Set -> Set -> Set ; +def Conj A B = Sigma A (\x -> B) ; + +fun Neg : Set -> Set ; +def Neg A = Impl A Falsum ; + +-- constructors + +data + i : ({A,B} : Set) -> El A -> El (Plus A B) ; + j : ({A,B} : Set) -> El B -> El (Plus A B) ; + + lambda : ({A} : Set) -> ({B} : El A -> Set) -> ((x : El A) -> El (B x)) -> El (Pi A B) ; + + pair : ({A} : Set) -> ({B} : El A -> Set) -> (x : El A) -> El (B x) -> El (Sigma A B) ; + + Zero : El Nat ; + Succ : El Nat -> El Nat ; + + r : (A : Set) -> (a : El A) -> El (Id A a a) ; + +-- selectors + +fun D : ({A,B} : Set) -> ({C} : El (Plus A B) -> Set) -> + (c : El (Plus A B)) -> + ((x : El A) -> El (C (i A B x))) -> + ((y : El B) -> El (C (j A B y))) -> + El (C c) ; +def + D _ _ _ (i _ _ a) d _ = d a ; + D _ _ _ (j _ _ b) _ e = e b ; + +fun app : ({A} : Set) -> ({B} : El A -> Set) -> El (Pi A B) -> (a : El A) -> El (B a) ; +def app _ _ (lambda _ _ f) a = f a ; + +fun + p : ({A} : Set) -> ({B} : El A -> Set) -> (_ : El (Sigma A B)) -> El A ; + q : ({A} : Set) -> ({B} : El A -> Set) -> (c : El (Sigma A B)) -> El (B (p A B c)) ; +def + p _ _ (pair _ _ a _) = a ; +---- q _ _ (pair _ _ _ b) = b ; ---- doesn't compile yet AR 13/9/2011 +---- q A B c = E A B (\z -> B (p A B z)) c (\x,y -> y) ; ---- neither does this: {x <> p A B (pair A B x y)} + +fun E : ({A} : Set) -> ({B} : El A -> Set) -> ({C} : El (Sigma A B) -> Set) -> + (c : El (Sigma A B)) -> + ((x : El A) -> (y : El (B x)) -> El (C (pair A B x y))) -> + El (C c) ; +def E _ _ _ (pair _ _ a b) d = d a b ; + +fun + R0 : ({C} : El Falsum -> Set) -> (c : El Falsum) -> El (C c) ; + +fun + Rec : ({C} : El Nat -> Set) -> + (c : El Nat) -> + (El (C Zero)) -> + ((x : El Nat) -> (El (C x)) -> El (C (Succ x))) -> + El (C c) ; +def + Rec _ Zero d _ = d ; + Rec C (Succ x) d e = e x (Rec C x d e) ; + +fun J : (A : Set) -> (a,b : El A) -> (C : (x,y : El A) -> El (Id A x y) -> Set) -> + (c : El (Id A a b)) -> + (d : (x : El A) -> El (C x x (r A x))) -> + El (C a b c) ; +def J _ _ _ _ (r _ a) d = d a ; + +-- tests + +fun one : El Nat ; +def one = Succ Zero ; + +fun two : El Nat ; +def two = Succ one ; + +fun plus : El Nat -> El Nat -> El Nat ; +def plus a b = Rec (\x -> Nat) b a (\x,y -> Succ y) ; + +fun times : El Nat -> El Nat -> El Nat ; +def times a b = Rec (\x -> Nat) b Zero (\x,y -> plus y x) ; + +fun exp2 : El Nat -> El Nat ; -- 2^x +def exp2 a = Rec (\x -> Nat) a one (\x,y -> plus y y) ; + +fun fast : El Nat -> El Nat ; -- fast (Succ x) = exp2 (fast x) +def fast a = Rec (\x -> Nat) a one (\_ -> exp2) ; + +fun test : El Nat ; +def test = fast (fast two) ; + +}
\ No newline at end of file |