# 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`

If you're using jar with java, use the following instead:

`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, use`open import X`

to unqualify. This is short for`import X`

followed by`open X`

. - Aya supports restricted import
`open import X using (x)`

(this only imports`x`

from`X`

) you may also use`open import X hiding (x)`

to import everything except`x`

from`X`

. - 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`

In Aya (we replaced the keyword `data`

with `inductive`

because we want to use it as a package name):

`inductive 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 (intentionally not called `+`

to avoid name clash with Prelude):

```
(<+>) :: 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 <*>
```

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`

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
```

When we only need to pattern match on a subset of the parameters, we can use the `elim`

keyword:

```
example def infixl [+] (a n : Nat) : Nat elim a
| 0 ⇒ n
| suc m ⇒ suc (m [+] n)
```

## Type-level programming

In Haskell:

```
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 have`Set`

, and`ISet`

. 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 inductive 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 inductive 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:

```
inductive 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, I don't remember exactly
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 inductive 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.

## Overlapping patterns

There is one more bonus: in Aya, you may modify the definition of `<+>`

to be:

```
overlap def infixl <+> Nat Nat : Nat
| 0, n => n
| n, 0 => n
| suc m, n => suc (m <+> n)
```

It says we not only compute `0 + n = n`

, but when the first parameter is neither `0`

nor `suc`

, we may take a look at the second parameter and seek for other potential computations. This is completely useless at runtime, but very good for type checking. For instance, we may want a `Vec`

of size `n`

, and what we have is some `Vec`

of size `n + 0`

. Then having `n + 0`

to directly reduce to `n`

is very useful, otherwise we will need to write a conversion function that does nothing but changes the type, or use `unsafeCoerce`

.

With `n + 0 = n`

judgmentally, we now have more possibilities. For instance, we can make `xs ++ nil = xs`

. This involves in two steps: we first turni `++`

into a `overlap def`

, then we add the following clause to `++`

:

`| xs, nil => xs`

This makes `++`

compute on more cases too.

For more information about this feature, checkout the tutorial for proof assistant users.