Sit: size-irrelevant types
A prototype dependently-typed language with sized natural numbers
Sit parses and typechecks .agda that conform to the Sit language syntax.
Syntax (excerpt):
--- Lexical stuff --- Single line comment {- Block comment -} --; --- End of declaration (mandatory) f_x'1 --- identifiers start with a letter, then have letters, digits, _ and ' --- Declarations x : T --; --- type signature x = t --; --- definition open import M --; --- ignored, for Agda compatibility --- Sit specifics oo --- infinity size i + 1 --- successor size Nat a --- type of natural numbers below size a zero a --- number zero (a is size annotation) suc a n --- successor of n (a is size annotation) forall .i -> T --- irrelevant size quantification forall ..i -> T --- relevant size quantification fix T t n --- recursive function over natural numbers --- T: return type --- t: functional --- n: natural number argument \{ (zero _) -> t; (suc _ x) -> u } --- case distinction function --- Inherited Agda syntax U -> T --- non-dependent function type (x y z : U) -> T --- dependent function type \ x y z -> t --- lambda-abstraction t u --- application Set --- first universe Set1 --- second universe Set a --- universe of level a
Limitations
Sit only understands a tiny subset of the Agda language.
Sit does not understand layout, instead each declaration has to be terminated with
comment --;.
Installation
Requires GHC and cabal, for instance via the Haskell Platform. In a shell, type
cabal install
Test
In a shell, type
Sit.bin test/Test.agda
Example
This is the addition function in Sit:
--- Addition of natural numbers
plus : forall .i -> Nat i -> Nat oo -> Nat oo --;
plus = \ i x y ->
fix (\ i x -> Nat oo)
(\ _ f -> \
{ (zero _) -> y
; (suc _ x) -> suc oo (f x)
})
x