[Agda] Newbie questions after reading Dependently Typed Programming in Agda

[Samuel Gélineau]

On Tue, Oct 12, 2010 at 5:14 PM, Oscar Finnsson
<oscar.finnsson at gmail.com> wrote:
> I've got some newbie questions after reading (and writing the code in)
> Dependently Typed Programming in Agda.

Wow, you have a lot of questions! I know the answer to a couple. I'm
not as terse as Thorsten, but since you are new to agda, this is
probably a good thing.


> 2. What does it mean when a function declaration got a signature like
> > isTrue  : Bool → Set
> Is isTrue a decomposer? Is the type checker aware that True and False
> are the only valid types from isTrue?

isTrue is a function from Bool to Set, nothing more, nothing less. The
type-checker is aware that (isTrue false) yields False and (isTrue
true) yields True, but given only (isTrue x), the type checker doesn't
know that the expression can only yield True or False. For this
reason, you cannot pattern-match on a value of type (isTrue x) unless
you pattern-match on x first.


> Why is
> > isTrue : Bool -> Set
> > isTrue true = True
> > isTrue false = False
> valid but not the reverse, i.e.
> > isBool : Set -> Bool
> > isBool True = true
> > isBool False = false
> isn't? Agda will complain about:
> "Unreachable clause
> when checking the definition of getBool"
> regarding the last case (isBool False).

You cannot pattern-match on values of type Set. Your isBool
implementation is equivalent to this one:

> isBool : Set -> Bool
> isBool x = true
> isBool y = false

so the second clause is indeed unreachable.

> It seems to accept
> > data Foo : Set where
> > checkIsTrue : (x : Bool) → (isTrue x) → Bool
> > checkIsTrue true True = false
> > checkIsTrue false Foo = true
> as complete but I think (and Agda can also accept) the last pattern
> match should be
> > checkIsTrue false False = true
> since "false Foo" cannot happen.

This time, your mistake is a bit more complicated. You are correct in
thinking that once x has been established to be true, the compiler
knows that the type (isTrue x) is now the type True, and similarly
when x has been established to be false. I can see that you are trying
to pattern-match on the result of (isTrue x) in order to ensure that
the result is what you expect, however, that's not what your code is
doing. You are writing a function of type Bool -> isTrue x -> Bool.
When x is true, you can assume you are writing a function of type Bool
-> True -> Bool, and when x is false, you can assume you are writing a
function of type Bool -> False -> Bool. In your code, however, you use
True, Foo and False as pattern names, so you act as if your function
had type Bool -> Set -> Bool, which is incorrect.

Nevertheless, for the same reason as before, your code is equivalent to this:

> checkIsTrue : (x : Bool) -> (isTrue x) -> Bool
> checkIsTrue true x = false
> checkIsTrue false y = true

which is why agda doesn't complain even if you use a variable name like "Foo".


> 10. Regarding absurd patterns (p. 9). I don't understand why Fin zero
> is a valid type. Shouldn't all FinS begin with Fin (suc ...) and isn't
> dependent typing about enforcing this?

Fin has type Nat -> Set, and therefore Fin x is valid for any value x
of type Nat. In particular, Fin zero is valid, but it is not
inhabited, just like False is a valid but uninhabited type.


> 16. Why is False defined as
> > data False : Set where
> while True is defined as
> > record True : Set where
> and why aren't both using the same sort of definition (data or record)?

Because it's shorter and more symmetrical that way. An alternate
definition of True, using data, would be

> data True : Set where
>   tt : True

The point is that True should have exactly one inhabitant, and a
record with no members has exactly one inhabitant, namely, (record
{}).

> 17. Why is [_] (in Data.List) defined as
> > forall {a} {A : Set a} -> A -> List A
> and not simply
> > {A : Set} -> A -> List A
> and what does "Set a" mean? It seems to have something to do with
> --universe-polymophism... .

Nat has type Set which has type Set1 which has type Set2 and so on. We
used to define multiple versions of everything, like

> data List (A : Set) : Set where
>   nil : List A
>   cons : A -> List A -> List A
>
> [_] : {A : Set} -> A -> List A
> [ x ] = cons x nil
>
>
> data List1 (A : Set1) : Set1 where
>   nil : List1 A
>   cons : A -> List1 A -> List1 A
>
> [_] : {A : Set1} -> A -> List1 A
> [ x ] = cons x nil

and so on, but thanks to universe polymorphism, we can now define a
single generic version for everything.


> 18. Why is the type declaration for apply (in the paper/tutorial by Ulf Norell):
> > (A : Set)(B : A -> Set) -> ((x : A) -> B x) -> (a : A) -> B a
> and not
> > (A : Set)(B : A -> Set) -> (A -> B A) -> A -> B A
> or even
> > {A B : Set} -> (A -> B) -> A -> B
> analogous to the declaration for map?

Watch out! ((x : A) -> B x) is not at all the same as (A -> B A). In
the first, B is a function of type A -> Set, while in the second, B is
a function of type Set -> Set. You must not confuse a variable of type
A with the type A itself!

The reason apply is defined this way is to make it possible to apply a
function f which has a dependent type. If apply and f had type

> apply : (A B : Set) (A -> B) -> A -> B
> f : (x : Nat) -> Fin x

(note that I made the arguments A and B explicit)
and you wanted to apply the function f, how would you instantiate A
and B? You cannot simply say

> f-of-one : Fin 1
> f-of-one = apply Nat (Fin x) f 1

because x is not in scope at this point. With the more complicated type

> apply : (A : Set)(B : A -> Set) -> ((x : A) -> B x) -> (a : A) -> B a

it is now possible to instantiate A and B:

> f-of-one : Fin 1
> f-of-one = apply Nat (λ x → Fin x) f 1


> 21. What is the difference between parameters and indices of a
> datatype (except syntactically)? Is there something you can do with
> one that you cannot do with the other? When should I preferre one over
> the other?

As a rule, if all your constructors end in (Foo A), then A should be a
parameter. If some of your constructors need to specialize A by
returning something like (Foo Bool), then A must be an index.


Specializing is useful when doing something like GADTs, where
constructors create values with different types:

> data Foo : Nat -> Set where
>   foo-zero : Foo 0
>   foo-one  : Foo 1

When all your constructors end in (Foo A), you can use either
parameters or indices:

> data List (A : Set) : Set where
>   nil : List A
>   cons : A -> List A -> List A

> data List' : Set -> Set1 where
>   nil : {A : Set} -> List A
>   cons : {A : Set} -> A -> List A -> List A

But if you use indices then you have to repeat the {A : Set} argument
for every constructor, and List' must have type (Set -> Set1) instead
of (Set -> Set).


hope this helps,
– Samuel