Sigil

overview • documentation • tooling

What Is Sigil?

Sigil is an experimental language investigating the intersection of dependent types and interactive programming. Sigil aims to unite the interactive tooling of lisps with the certainty of static types.

This code snippet shows code that currently type-checks & runs under Sigil. If you're interested in the ambitions of the project, you can see some forward-looking examples here. 

⍝ The natural numbers (0 1, 2, ...)
ℕ ≜ μ N ⮜ 𝕌.
  zero ⮜ N      ⍝ the number zero
  succ ⮜ N → N  ⍝ given a number n, succ n represents n + 1


⋳ Constructors are prepended with a ':', so we
  get the following definitions of numbers
  0 → :zero
  1 → :succ :zero
  2 → :succ (:succ :zero)
  3 → :succ (:succ (:succ :zero))
  etc. ⋻ 

⍝ The values zero and succ are similar to :zero and :succ, but with more type information. 
zero ≜ :zero ﹨ ℕ
succ ≜ :succ ﹨ ℕ 


⍝ The φ is combines pattern-matching and recursion into a single expression
⍝ • The variable (rec) bound by φ names a recursive function
⍝ • The argument (m) is the initial value provided to the recursive function   
_+_ ⮜ ℕ → ℕ → ℕ
_+_ n m ≜ φ rec ⮜ ℕ → ℕ, m.
  :zero → n
  :succ i → succ (rec i)


⍝ Sample usage
two ≜ succ (succ zero)
four ≜ two + two

Running the Above Example

Assume the above code is in a file called test.sl. Then, we might run/test it with the following interactive session: 

$> sigil interactive-line
> ;load test.sl 
> ;import test.(..)
> two + four
val: :succ (:succ (:succ (:succ (:succ (:succ :zero)))))
type: [test, ℕ]
> ;q