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]

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

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
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 Anonymous
Maintainer Anonymous
Revised Revision 1 made by HerbertValerioRiedel at 2018-02-01T12:19:03Z
Category Dependent types
Home page NONE
Source repo head: git clone NONE
Uploaded by AndreasAbel at 2017-05-15T14:56:23Z
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 not available [build log]
Last success reported on 2017-05-15 [all 3 reports]

Readme for Sit-0.2017.2.26

[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