# Sit

Prototypical type checker for Type Theory with Sized Natural Numbers

https://github.com/andreasabel/Sit

 LTS Haskell 22.29: 0.2023.8.3 Stackage Nightly 2024-07-16: 0.2023.8.3 Latest on Hackage: 0.2023.8.3

See all snapshots Sit appears in

LicenseRef-OtherLicense licensed and maintained by
This version can be pinned in stack with:Sit-0.2023.8.3@sha256:99efbca262f0292d71e389b79ed7a4df4359900df62e817ab532c7ec2db3b510,2900

#### Module documentation for 0.2023.8.3

Depends on 6 packages(full list with versions):
Used by 1 package in nightly-2024-06-18(full list with versions):

# 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

## 0.2023.8.3

• support GHC 7.8 - 9.8.1-alpha1
• remove generated Lex.hs and Par.hs as they get stale

## 0.2022.3.18

• support GHC 7.8 - 9.2
• add missing build-tool dependencies alex and happy

## 0.2021.1.18

• support GHC 7.8 - 8.10
• added minimal cabal test suite (1 test)