Hackage :: [Package]

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]

Modules

[Index] [Quick Jump]

Downloads

Maintainer's Corner

Package maintainers

For package maintainers and hackage trustees

Candidates

Versions [RSS] 0.2017.2.26, 0.2017.5.1, 0.2017.5.2, 0.2021.1.18, 0.2022.3.18, 0.2023.8.3
Change log CHANGELOG.md
Dependencies array (>=0.3 && <1), base (>=4.7 && <5), containers (>=0.3 && <1), data-lens-light (>=0.1.2.2 && <0.2), mtl (>=2.2.1 && <3), Sit [details]
License LicenseRef-OtherLicense
Author Andreas Abel <andreas.abel@gu.se>
Maintainer Andreas Abel <andreas.abel@gu.se>
Category Dependent types
Home page https://github.com/andreasabel/Sit
Source repo head: git clone https://github.com/andreasabel/Sit
Uploaded by AndreasAbel at 2022-03-18T14:29:34Z
Distributions LTSHaskell:0.2023.8.3, NixOS:0.2023.8.3, Stackage:0.2023.8.3
Reverse Dependencies 1 direct, 0 indirect [details]
Executables Sit.bin
Downloads 2976 total (21 in the last 30 days)
Rating (no votes yet) [estimated by Bayesian average]
Your Rating
  • λ
  • λ
  • λ
Status Docs uploaded by user
Build status unknown [no reports yet]

Readme for Sit-0.2022.3.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

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