Sigil Overview

Comments are denoted with either the '⍝' symbol (for single line comments) or the '⋳' and '⋻' symbols for multi-line comments.

⍝ This is a comment

⋳ This is the start of a multi-line comment
  it continues here...
  ... and ends here ⋻

The sigil langauges feature a series of hierarchical universes, typed 𝕌 = 𝕌₀, 𝕌₁, 𝕌₂, ….

As a dependently-typed lambda calculus, Sigil has functions and the dependent product type. Use λ to start a function, followd by one or more arguments, which are (optionally annotated) symbols (annotations use the ⮜). A simple identity function would look like:

⍝ The identity function
λ A (x ⮜ A) → A

⍝ The identity function's type
(A ⮜ 𝕌) → A → A

Parameters (variables) can use underscores to associate themselves with a particular fixity. There is currently no way of declaring precedence.

⍝ infix is allowed
λ _+_ n m → n + m

⍝ prefix is allowed (and is also the default, so the underscore is unnecessary)
λ f_ x → f x

⍝ postfix is allowed
λ n _! → n !

⍝ closed is allowed
λ ⌊_⌋ x → ⌊ x ⌋

⍝ can be combined
λ if_then_else_ c e1 e2 → if c then e1 else e2

Inductive types are probably the most distinct from what you might expect. Inductive types are declared with the μ keyword. This is followed by the name of the type you wish to declare (in the below example, 'N'), alonf with its' kind. On a newline (and indented) you can then declare any number of constructors. IMPORTANT: The name (below, N), is only bound in the inductive type declaration.

μ N ⮜ 𝕌.
  zero ⮜ N
  succ ⮜ N → N

Inductive constructors must be prefixed via a colon ':' character, and must be paired with the type they are from. If we imagine that 'N' is bound the the type above, then the following are valid inductive values:

:zero ﹨ N
(:succ ﹨ N) (:zero ﹨ N)

This is important to note when doing pattern-matching, as patterns also use the colon prefix. The pattern-matching construct is also somewhat unusual, in that it involves simultaneously defining a recursive function and immediately invoking it. The induction term uses the 'φ' keyword, followed by the name and type of the recursive function that you are defining. Then, after a comma ',' provide the value that the function is being called with. As an example, the 'add' function would be defined as follows:

λ n m → φ rec ⮜ N → N, m. 
  :zero → n
  :succ → succ (rec i)

Definitions are given as a name followed by the '≜' keyword, and then the expression (value) which you want to define. For example, the below assigns the Natural number type (used earlier) to the symbol 'ℕ'.

ℕ ≜ μ M ⮜ 𝕌.
  zero ⮜ M
  succ ⮜ M → M

Definitions can also come with annotations beforehand, allowing annotations to be omitted from function arguments:

id ⮜ (A ⮜ 𝕌) → A → A
id ≜ λ A x → x

Function definitions can also use a list of names before the '≜' as arguments to the function:

_+_ ⮜ ℕ → ℕ → ℕ
_+_ n m ≜ φ rec ⮜ ℕ → ℕ, m.
  :zero → n
  :succ i → succ (rec i)

Tip: define utility funtions/values that bundle an inductive constructor to make defining inductive values more convenient.

zero ≜ :zero ﹨ ℕ
succ ≜ :succ ﹨ ℕ

An equality query will succeed if the two expressions are equal. For example, the below query succeeds.

𝕌 ≅ 𝕌

A habitation query will succeed if the two left hand expression is a value whose type is the right hand expression. For example, the below query succeeds.

𝕌 ∈ 𝕌₁

A conjoined qieru will succeed if both sub-queries succeed, and fail otherwise. For example, the below query succeeds.

(𝕌 ∈ 𝕌₁) ∧ (𝕌 ≅ 𝕌)

An existential query ∃ x ⮜ E. Q will succeed if there is some value of x which will make Q succeed. If it does suceed, then the value of x that it derives will be returned. As an example, the below query will succeed "solved with n ↦ :succ :zero".

∃ n ⮜ ℕ. n + one ≅ two

A universal query ∀ x ⮜ E. Q will succeed if all values x of type E will make Q succeed. They can be combined with existential queries. As an example, the below query will succeed "solved with m ↦ n".

∀ n ⮜ ℕ. ∃ m ⮜ n ≅ m