Sit: Prototypical type checker for Type Theory with Sized Natural Numbers

[ dependent-types, library, program ] [ Propose Tags ]

Sit = Size-irrelevant types

Sit is a prototypical language with an Agda-compatible syntax. It has dependent function types, universes, sized natural numbers, and case and recursion over natural numbers. There is a relevant and an irrelevant quantifier over sizes. For an example, see file test/Test.agda.

[Skip to Readme]
Versions [RSS] [faq] 0.2017.2.26, 0.2017.5.1, 0.2017.5.2, 0.2021.1.18
Change log
Dependencies array (>=0.3 && <1), base (>=4.7 && <5), containers (>=0.3 && <1), data-lens-light (>= && <0.2), mtl (>=2.2.1 && <3), Sit [details]
License LicenseRef-OtherLicense
Author Andreas Abel <>
Maintainer Andreas Abel <>
Revised Revision 1 made by AndreasAbel at 2021-01-18T14:25:41Z
Category Dependent types
Home page
Source repo head: git clone
Uploaded by AndreasAbel at 2021-01-18T11:44:13Z
Distributions LTSHaskell:0.2021.1.18, NixOS:0.2021.1.18, Stackage:0.2021.1.18
Executables Sit.bin
Downloads 2456 total (13 in the last 30 days)
Rating (no votes yet) [estimated by Bayesian average]
Your Rating
  • λ
  • λ
  • λ
Status Hackage Matrix CI
Docs available [build log]
Last success reported on 2021-01-18 [all 1 reports]


[Index] [Quick Jump]


Note: This package has metadata revisions in the cabal description newer than included in the tarball. To unpack the package including the revisions, use 'cabal get'.

Maintainer's Corner

For package maintainers and hackage trustees


Readme for Sit-0.2021.1.18

[back to package description]

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


Sit only understands a tiny subset of the Agda language. Sit does not understand layout, instead each declaration has to be terminated with comment --;.


Requires GHC and cabal, for instance via the Haskell Platform. In a shell, type

  cabal install


In a shell, type

  Sit.bin test/Test.agda


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)