So you know some Haskell
Great. I expect you to know something about GHCi and algebraic data types. This is an Aya tutorial for Haskell programmers. If you find a bug, open an issue on GitHub!
Working with the REPL
Aya has a REPL that works similar to GHCi. You can start it by running aya -i
in your terminal, and you can start typing definitions or expressions.
aya -i
aya -i
If you're using jar with java, use the following instead:
java --enable-preview -jar cli-fatjar.jar -i
java --enable-preview -jar cli-fatjar.jar -i
In the REPL, you can use :l
to load a file, :q
to quit, and :?
to get help. Use :t
to show the type. Since it's dependent type, you can toggle normalization levels by :normalize
followed by NF
, WHNF
, or NULL
(don't normalize).
To work multiline, use the pair :{
and :}
-- same as GHCi.
Aya supports pretty-printing of any terms, including ✨lambdas✨. Note that Aya does not automatically support generic lambdas, so typing \x => x
would not work. You need to specify the type of x
, like \(x : Int) => x
.
Aya support fn
as an alias to \
instead of λ
, similar to Coq and Lean (but not Agda). This is because users (especially mathematicians) are likely to use λ
as a variable name. Similarly, we used Fn
over Pi
or Π
for the same reason.
Working with projects
Read project-tutorial, it is very short. It is recommended to practice the following with an Aya project in VSCode, see vscode-tutorial.
About modules:
- Aya module names are separated by
::
, not.
. - Aya infers the module names automagically, using the same rule as of Haskell.
- Aya imports (
import X
) are qualified by default, useopen import X
to unqualify. This is short forimport X
followed byopen X
. - Aya supports restricted import
open import X using (x)
(this only importsx
fromX
) you may also useopen import X hiding (x)
to import everything exceptx
fromX
. - Aya supports renamed import
open import X using (x as y)
and the meaning is obvious. - To re-export, use a
public open
.
Ok, let's write some code!
Programming in Aya
Natural numbers. In Haskell:
data Nat = Zero | Suc Nat
data Nat = Zero | Suc Nat
In Aya:
data Nat | zero | suc Nat
We don't enforce capitalization of constructors. The constructors need to be qualified (like Nat::zero
) to access. As you may expect, Nat
automatically becomes a module, so we can use open
and public open
to unqualify the constructors.
Bonus: if you define a data type that looks like Nat
, then you can use numeric literals.
Functions are defined with def
, followed by pattern matching. Consider this natural number addition in Haskell:
(<+>) :: Nat -> Nat -> Nat
Zero <+> n = n
Suc m <+> n = Suc (m <+> n)
infixl 6 <+>
(<+>) :: Nat -> Nat -> Nat
Zero <+> n = n
Suc m <+> n = Suc (m <+> n)
infixl 6 <+>
In Aya (remember the numeric literal thing?):
open Nat
def infixl <+> Nat Nat : Nat
| 0, n ⇒ n
| suc m, n ⇒ suc (m <+> n)
There are plenty of differences. Let's go through them one by one.
The infixl
declares <+>
to be a left-associative infix operator. Other options include infix
, infixr
, fixl
, and fixr
. Without it, the function will work the same as normal function. Unlike Haskell, we do not distinguish "operator" names and "function" names.
We do not use a number to denote precedence, but a partial order. This allows arbitrary insertion of new precedence level into previously defined ones. Say you want <+>
to have a lower precedence than <*>
, you can do:
def infixl <+> Nat Nat : Nat
/// .... omitted
looser <*>
def infixl <+> Nat Nat : Nat
/// .... omitted
looser <*>
You also have tighter
, with the obvious meaning.
The parameters and the return type are separated using :
. The parameter types can be written directly, without ->
. Aya allow naming the parameters like this:
def oh (x : Nat) : Nat
def oh (x : Nat) : Nat
These names can be used for one-linear function bodies:
def oh (x : Nat) : Nat ⇒ x
Aya supports a painless version of the section syntax, where the top-level does not need parentheses. See the following REPL output (the underscored names are internally generated variable names. If you have an idea on how to make them better, open an issue and let's discuss!).
> 1 <+>
suc
> <+> 1
λ _7 ⇒ _7 <+> 1
> 1 <+> 1
suc 1
> 2 <+>
λ _5 ⇒ suc (suc _5)
> <+> 2
λ _7 ⇒ _7 <+> 2
> 1 <+>
suc
> <+> 1
λ _7 ⇒ _7 <+> 1
> 1 <+> 1
suc 1
> 2 <+>
λ _5 ⇒ suc (suc _5)
> <+> 2
λ _7 ⇒ _7 <+> 2
Aya also supports pattern matching expressions -- using the match
keyword. Example:
def pred (x : Nat) : Nat ⇒
match x {
| suc a ⇒ a
| 0 ⇒ 0
}
Type-level programming
In Haskell:
id :: a -> a
id x = x
id :: a -> a
id x = x
In Aya:
def id {A : Type} (x : A) ⇒ x
Observations:
- Type parameters have to be explicitly qualified using curly braces.
- Curly braces denote parameters that are omitted (and will be inferred by type checker) in the pattern matching and invocations. So, parentheses denote parameters that are not omitted.
- Apart from
Type
, we also haveSet
,Prop
, andISet
. For now, don't use the others.
Type constructors are like {F : Type -> Type}
(and yes, the ->
denotes function types, works for both values and types), very obvious. Definition of Maybe
in Aya:
open data Maybe (A : Type)
| nothing
| just A
Here, (A : Type)
is an explicit parameter, because you write Maybe Nat
, not just Maybe
.
There is a way to automagically insert the implicit parameters -- the variable
keyword.
variable A : Type
// Now, since you are using A, so Aya inserts {A : Type}
example def id (x : A) ⇒ x
Aya supports type aliases as functions. For example, we may define the type of binary operators as a function:
def BinOp (A : Type) ⇒ A → A → A
Then, we can define <+>
as:
example def infixl <+> : BinOp Nat
| 0, n ⇒ n
| suc m, n ⇒ suc (m <+> n)
Type families
In Aya, type families are functions. Consider the following code (they are using the variable A
defined above):
// Unit type
open data Unit | unit
// A type family
def FromJust (x : Maybe A) : Type
| just a ⇒ A
| nothing ⇒ Unit
// A function that uses the type family
def fromJust (x : Maybe A) : FromJust x
| just a ⇒ a
| nothing ⇒ unit
And fromJust (just a)
will evaluate to a
. In Haskell, you need to use some language extensions alongside some scary keywords. These functions are available in constructors, too:
data Example (A : Type)
| cons (x : Maybe A) (FromJust x)
It is recommended to play with it in the REPL to get a feel of it.
There is a famous example of dependent types in Haskell -- the sized vector type:
{-# LANGUAGE GADTs #-}
{-# LANGUAGE DataKinds #-}
-- Maybe you need more, but I don't recall. Sorry.
data Vec :: Nat -> Type -> Type where
Nil :: Vec Zero a
(:<) :: a -> Vec n a -> Vec (Suc n) a
infixr :<
{-# LANGUAGE GADTs #-}
{-# LANGUAGE DataKinds #-}
-- Maybe you need more, but I don't recall. Sorry.
data Vec :: Nat -> Type -> Type where
Nil :: Vec Zero a
(:<) :: a -> Vec n a -> Vec (Suc n) a
infixr :<
In Aya, we have a better syntax:
open data Vec (n : Nat) (A : Type)
| 0, A ⇒ nil
| suc n, A ⇒ infixr :< A (Vec n A)
The :<
constructor is defined as a right-associative infix operator. And yes, you can define like vector append painlessly:
variable m n : Nat
def infixr ++ (Vec n A) (Vec m A) : Vec (n <+> m) A
| nil, ys ⇒ ys
| x :< xs, ys ⇒ x :< xs ++ ys
tighter :<
Imagine how much work this is in Haskell.