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