PiSigma

This is a prototype of the sytem presented in this draft .

The syntactic differences are explained in the example program.

Edit your program:

{- A PiSigma program consists in a list of declarations and definitions. The main difference with the draft paper is that each entry is terminated bi a dot and that labels are preceded by a quote. -} {- Definition of Bool, as a set of 2 labels -} Bool : Type. Bool = {'true , 'false}. {- Recursive definition of natural numbers.-} Nat : Type. Nat = tag : {'Z, 'S}; ! case tag of {'Z -> [ {'Unit} ] | 'S -> [ Nat] }. zero : Nat. zero = 'Z, 'Unit. succ : Nat -> Nat. succ = \ n -> 'S, n. one : Nat. one = succ zero. two : Nat. two = succ one. plus : Nat -> Nat -> Nat. plus = \ n -> \ m -> split (tag, n') = n in ! case tag of { 'Z -> [ m ] | 'S -> [ succ (plus n' m)] } . {- The type of streams. - Case corresponds to the underlined case of the draft. Case ... of ... = ! case ... of [...] -} Stream : Type -> Type. Stream = \ A -> tag : {'Cons,' Last } ; a : A ; Case tag of {'Cons -> $ (Stream A) | 'Last-> {'Unit}}. {- Infinite streams of zeros -} zeros : Stream Nat. zeros = 'Cons, zero, [ zeros ]. {- map on Streams -} smap : (A : Type) -> (B : Type) -> (A -> B) -> Stream A -> Stream B. smap = \ A -> \ B -> \ f -> \ as -> split (tag, node) = as in split (el, as') = node in ! case tag of { 'Cons -> [ 'Cons,f el, [smap A B f !as' ] ] | 'Last -> ['Last, f el, 'Unit]}. ones : Stream Nat. ones = smap Nat Nat succ zeros. {- Vectors as function from their size to Type -} Vec : Nat -> Type -> Type. Vec = \ n -> \ A -> split (nl,n') = n in Case nl of { 'Z -> {'Unit} | 'S -> (a : A ; Vec n' A) }. vappend : (m : Nat) -> (n:Nat) -> (A :Type) -> Vec m A -> Vec n A -> Vec (plus m n) A. vappend = \ m -> \ n-> \ A -> \ as -> \ bs -> split (ml,m') = m in Case ml of { 'Z -> bs | 'S -> split (a,as') = as in a , (vappend m' n A as' bs) }. {- Vectors represented with equality constraints. The equality constraint is written || and not | as in the draft. -} Vec : Nat -> Type -> Type. Vec = \n -> \ A -> tag : {'Nil, 'Cons} ; Case tag of { 'Nil -> l : {'Unit} || ('Z,'Unit) = n | 'Cons -> a : A ; m : Nat ; l : Vec m A || ('S,m) = n }. head : (A : Type) -> (n : Nat) -> Vec (succ n) A -> A. head = \ A -> \ n -> \ vec -> split (tag,node) = vec in case tag of {'Nil -> case node of {'Unit -> #} |'Cons -> split (a,tail) = node in a}. tail : (A : Type) -> (n : Nat) -> Vec (succ n) A -> Vec n A. tail = \ A -> \ n -> \ vec -> split (tag,node) = vec in case tag of {'Nil -> case node of {'Unit -> #} |'Cons -> split (a,tail') = node in split (m, tail) = tail' in tail }. append : (A : Type) -> (n : Nat) -> (m : Nat) -> Vec n A -> Vec m A -> Vec (plus n m) A. append = \ A -> \ n -> \ m -> \ v1 -> \ v2 -> split (tag, node) = v1 in Case tag of {'Nil -> case node of {'Unit -> v2} |'Cons -> split (a,node') = node in split (n', tail) = node' in 'Cons, a, (plus n' m), append A n' m tail v2}. {- List and witnessing filter -} List : Type -> Type. List = \ A -> ( l : { 'Nil, 'Cons }; Case l of { 'Nil -> {'Unit} | 'Cons -> ( x : A ; List A) } ). filter : (A:Type) -> (P : (A -> Bool)) -> List A -> List (a : A || P a = 'true). filter = \ A -> \ p -> \ as -> split (las,abs) = as in Case las of { 'Nil -> ('Nil , 'Unit) | 'Cons -> split (a,bs) = abs in Case p a of { 'true -> ('Cons, a , filter A p bs) | 'false -> filter A p bs }}. {- An inductive-recursive universe -} U : Type. el : U -> Type. U = (l : {'Typ, 'Pi} ; Case l of {'Typ -> {'Unit} | 'Pi -> a : U ; (el a -> U) }). el = \ a -> split (l,a') = a in case l of {'Typ -> U | 'Pi -> split (d , c) = (a') in ((x : el d) -> el (c x))}. {- A n-ary additioner : adds numbers until it meets a 0 -} Add : Type. Add = (n : Nat) -> split (tag,nn) = n in Case tag of { 'Z -> Nat | 'S -> Add}. add0 : Nat -> Add. add0 = \ n -> \ m -> split (tag, nn) = m in Case tag of {'Z -> n | 'S -> add0 (plus n m) }. add : Add. add = add0 zero. test : Nat. test = add one two two one zero. {- More strange and totally useless : adds numbers until the sum is even -} even : Nat -> Bool. odd : Nat -> Bool. even = \n -> split (tag, nn) = n in Case tag of { 'Z -> 'true | 'S -> odd nn}. odd = \n -> split (tag, nn) = n in Case tag of { 'Z -> 'false | 'S -> even nn}. Strange : Nat -> Type. Strange = \m -> (n : Nat) -> Case odd (plus m n) of { 'true -> Nat | 'false -> Strange (plus m n)}. strange0 : (n : Nat) -> Strange n. strange0 = \ n -> \ m -> Case odd (plus n m) of {'true -> plus n m | 'false -> strange0 (plus n m) }. strange : Strange zero. strange = strange0 zero. test2 : Nat. test2 = strange zero one.