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

[ dependent-types, 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 0.2017.2.26, 0.2017.5.1, 0.2017.5.2
Dependencies array (>=0.3 && <1), base (>=4.2 && <5), containers (>=0.3 && <1), data-lens-light (>=0.1.2.2 && <0.2), mtl (>=2.2.1 && <3) [details]
License LicenseRef-OtherLicense
Author Andreas Abel <andreas.abel@gu.se>
Maintainer Andreas Abel <andreas.abel@gu.se>
Revised Revision 2 made by HerbertValerioRiedel at Thu Feb 1 12:15:13 UTC 2018
Category Dependent types
Home page https://github.com/andreasabel/Sit
Source repo head: git clone https://github.com/andreasabel/Sit
Uploaded by AndreasAbel at Tue May 16 07:25:30 UTC 2017
Distributions NixOS:0.2017.5.2
Executables Sit.bin
Downloads 795 total (40 in the last 30 days)
Rating (no votes yet) [estimated by rule of succession]
Your Rating
  • λ
  • λ
  • λ
Status Docs not available [build log]
Last success reported on 2017-05-16 [all 3 reports]
Hackage Matrix CI

Downloads

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.2017.5.2

[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