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

[Thorsten Altenkirch]

Hi Oscar,

I may not be the best person to answer some of your questions but I just felt like having a go at you little quiz...

> 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

I think explicit parameters are only positional.

> 
> 2. What does it mean when a function declaration got a signature like
>> isTrue  : Bool → Set

It eats booleans and shits sets.

> Is isTrue a decomposer?

What is a decomposer?

> Is the type checker aware that True and False
> are the only valid types from isTrue?

Nope.

> 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

You can't match against a set, Agda just thinks that True and False a variables. The Haskell convention that capital letters indicate constructors does not apply to Agda.

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

Sure, it's just a catch all.

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

You are on the wrong track here.
> 
> 3. Is there any interpreter like ghci for Agda?

What is wrong with C-c C-n?

> 4. How can I make C-x C-l run faster (it's usually freezing emacs for
> 5-15 seconds)?

Good question.

> It seems to spend a lot of time in ghc. I suspect it's
> recompiling code from the Agda standard library every time.

I think it is just loading the library.

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

No, but you can generate html from Agda code with links to the definitions. It's a flag to the agda command line interface (--html).

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

I don't have this problem. I am using Aquamacs.

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

No, it is an impossible pattern. But if one would just leave out the line this would make the job harder for the pattern completeness checker.

> 
> 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 zero is a fine type, it is just empty.

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

This may be outdated.

Otherwise it is a good question. Many uses of type classes are covered by dependent types, but not all.

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

I am using Agda in a 3rd year course in Nottingham
http://www.cs.nott.ac.uk/~txa/g52ifr/
but I am not sure that's what you are looking for.

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

Pi types are dependent function types (x : A) → B x which were traditionally written as Π x : A . B x.
Sigma types are dependent product types (import Data.Product), in Agda Σ A (λ x → B x), traditionally
Σ x : A. B x.

As one rarely needs products in Haskell, one rarely uses Sigma types in Agda.

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

I think there is library for integers but these are not machine integers.

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

Somebody else better answers this.

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

I better leave this to Ulf. Certainly Agda is evolving quicker than its documentation....

> 
> 16. Why is False defined as
>> data False : Set where

False = the empty set is the set with no constructors.

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

True is the record with no fields, i.e. a one element set.

Using records to define True has the advantage that there is eta equality for records and hence elements of True can always be completed by the type checker.

There is no way to define False using records.

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

Oops, this doesn't type check, B eats As not sets. 

> or even
>> {A B : Set} -> (A -> B) -> A -> B
> analogous to the declaration for map?

This is the non-dependent apply. Btw there is also a dependent map. Another story.

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

Why should it be called something special?

> Are there any restrictions on what kind of
> constructors that are allowed?

Who told you that only constructors 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?
> 

Yes, just try it.

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

You only dot if you repeat variables.

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

If you can use parameters this is usually better (certainly saves quantifying over them in the constructor type).
But if you use the type at different instance this is not possible.

Parameters also behave differently wrt size (set levels) but this is maybe a more advanced topic.

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

what?

> but what are the second
> called and what are they typically used for?

Why do you need special names for things?

> Functions beginning with
> "Set" seems to only accept 1 pattern/1 value for Set. Is it so?

You can't match on Set.

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

Yes.


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

Yes, use mutual then indent. All the definitions then can be mutual recursive.

Actually it is a bit more subtle...

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

Tinkering is good. Have fun.

Thorsten

> 
> -- Oscar
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda

-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20101012/3ea8a0d5/attachment-0001.html