Popularity
3.5
Declining
Activity
0.0
Stable
6
2
0

Monthly Downloads: 23
Programming language: Haskell
License: LicenseRef-OtherLicense

Sit alternatives and similar packages

Based on the "Dependent Types" category.
Alternatively, view Sit alternatives based on common mentions on social networks and blogs.

Do you think we are missing an alternative of Sit or a related project?

Add another 'Dependent Types' Package

README

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