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

[Oscar Finnsson]

Hi,

I've got some newbie questions after reading (and writing the code in)
Dependently Typed Programming in Agda.

1. Is it possible to use "record syntax" (names parameters) for
functions even when the arguments aren't implicit? I.e. can I
construct named explicit arguments?
I would like to be able do something like:
> foo : (x : Nat) -> Nat
> answer = foo { x = 42 }
> answer2 = foo 42

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?
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). It's however accepting the
code if I remove the last isBool-pattern (False = false).
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. I'm clearly misunderstanding
something here since I thought that (isTrue x) should make sure that
the second argument is a valid value given a first value (i.e.
"checkIsTrue true True" should be a valid pattern while "checkIsTrue
true False" or "checkIsTrue true Foo" shouldn't).

3. Is there any interpreter like ghci for Agda?

4. How can I make C-x C-l run faster (it's usually freezing emacs for
5-15 seconds)? It seems to spend a lot of time in ghc. I suspect it's
recompiling code from the Agda standard library every time.

5. Which keywords got fancy utf-8 alternatives? I've found forall (∀)
and -> (→) so far. Any I've missed?

6. Is there any tool like Haddock for generating documentation?

7. Which font do you use in Emacs (Mac OS X)? Sometimes squares show
up (in the standard library) where it probably should be some utf-8
symbol.

8. How do you use {! !}? After running C-x C-l I receive suggestions
but can I somehow automatically insert them?

9. What is the value from an absurd pattern? ()? If it's (): what does
it mean? Something like Haskell's undefined?

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?

11. Is there anything like Haskell type classes in Agda? I've read
that there aren't but http://types2004.lri.fr/SLIDES/coquand.pdf seems
to indicate there are. Or are the slides just a proposal for new
functionality? If there are no type classes: can they be simulated
somehow using some Agda technique?

12. Is there any up-to-date tutorial/documentation for Agda?
"Dependently Typed Programming in Agda" was excellent as an
introduction but a bit dated (e.g. standard lib not the same).

13. What are Sigma and Pi that are mentioned sometimes? Googling them
is a bit hard... .

14. How do I construct integers (not Nat) and floats in Agda?
I understand that I can do something like
> answer : ℕ
> answer = 42
but that 42 won't be the same as an Haskell 42 right (i.e. Integer)?
How can I interface between Haskell primitives (Integer, Float) and
Agda primitives? All info I find is regarding Char and String. It is
somehow possible to convert an Haskell Integer into an Agda ℕ?

15. I cannot get the function "find" on p. 25 (Dependently Typed
Programming in Agda) to compile.
I get the error
> F (p x) !=< T (not (p (_226 p xs npxs x prf))) of type Set
> when checking that the expression falseIsFalse prf has type
> T (not (p (_226 p xs npxs x prf)))
regarding "falseIsFalse" on the last line in the function and I'm not
knowledgeable enough in Agda to understand that error message.
Not that it matters much, just thought someone (Ulf Norell?) might want to know.

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)?

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

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?

19. What is it called when you got a constructor in the declaration, e.g. in Vec
> _::_ : {n : Nat} -> A -> Vec A n -> Vec A (suc n)
where "suc" is used. What is "suc" (or similar constructors) called
when used in declarations? Are there any restrictions on what kind of
constructors that are allowed? n is a value so obviously values are
permitted as well. Are there any restrictions of which values can be
used or can arbitrary functions be used and would thus something like
> listToVec : {A : Set} -> (x: List A) -> Vec A (length x)
> listToVec [] = []
> listToVec x :: xs = x :: (listToVec xs)
be allowed?

20. In vmap₃ (p 9) why isn't nil dotted, i.e. replace
> vmap₃ zero f nil = nil
with
> vmap₃ zero f .nil = nil
since the only valid value for the third argument is nil?

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?

22. There seems to be some functions that end with "Set" and some that
begin with "Set", e.g.
> _==_  : {A : Set} → A → A → Set
> isTrue : Bool -> Set
and
> Matrix : Set -> Nat -> Nat -> Set
> Matrix A n m = Vec (Vec A n m)
The first are called deconstructors (or?) but what are the second
called and what are they typically used for? Functions beginning with
"Set" seems to only accept 1 pattern/1 value for Set. Is it so?

23. Am I correct in assuming that mixfix syntax demands that I got at
least 1 symbol between each argument, i.e.
> data  _ _][ : Bool -> Bool -> Set where
>  testing : (x : Bool) -> (y : Bool) -> x y ][
isn't permitted (I know the above isn't permitted, I'm just wondering
if I can somehow do something about my syntax to make something
similar)?

24. What are the scoping rules in Agda? Using functions, data types
and postulated values before they are defined doesn't seem to be OK.
Is it always top-down or can I somehow make functions be aware of
functions declared further down?

OK. It turned out to be more questions than I initially thought. Some
structured, some not so structured. I'll continue to tinker with Agda
but any guidance would be much appreciated.

-- Oscar