Hackage :: [Package]

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

This is a package candidate release! Here you can preview how this package release will appear once published to the main package index (which can be accomplished via the 'maintain' link below). Please note that once a package has been published to the main package index it cannot be undone! Please consult the package uploading documentation for more information.

[maintain] [Publish]

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]

Properties

Versions 0.2017.2.26, 0.2017.5.1, 0.2017.5.2, 0.2021.1.18, 0.2021.1.18, 0.2022.3.18, 0.2023.8.3
Change log CHANGELOG.md
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), 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 2021-01-18T11:32:40Z

Modules

[Index] [Quick Jump]

Downloads

Maintainer's Corner

Package maintainers

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

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