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

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

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

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

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`

,`Prop`

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

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.