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

[Oscar Finnsson]

Thanks everyone for all the great tips and pointers.


    What is wrong with C-c C-n?

Thanks for the tip. Didn't know that one.

    agda -I

Now I feel at home again.

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

Tried Aquamacs but I still got the same problem. ⟨ and  ⟩ don't show up
correctly. Anyone can recommend a good font?

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

I was under the impression that {! !} should find possible solutions and let
me insert them but maybe I've misunderstood the feature?

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

Thanks. After reading about [
http://en.wikipedia.org/wiki/Intuitionistic_Type_Theory] it became much
clearer.

    There is no way to define False using records.

Why not? Something to do with type theory (from now on I'll just refer to
type theory whenever I don't understand something :) )? If defining True
using record is such a good idea why isn't defining False using record a
good idea?

    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

I think I understand this one now. It's saying that the variable x will be
eaten at "B x" and the variable a will be eaten at "B a" right?

    You only dot if you repeat variables.

It finally became clear (I think).

    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.

OK. Makes sense. I'll just remember to think of GADTs.

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

And now I see it (mutual) all over the place. Didn't occur to me.

    http://www.cs.nott.ac.uk/~txa/g53cfr/

Good material, even though the difficulty increase between lecture 4 and 5
is a bit staggering.


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

I can see why this is useful.


    How can I interface between Haskell primitives (Integer, Float) and
Agda primitives?


http://wiki.portal.chalmers.se/agda/pmwiki.php?n=ReferenceManual.ForeignFunctionInterface

So I can use variables of type Integer, Float etc using "postulate" but if I
understand it correctly it's still impossible for me to express Integer and
Float-values in Agda (unless I first define some Haskell variables with
known integer-values, such as i1, i10, i100 etc that I map to Agda variables
and then construct new integers adding these predefined values, like: i13 =
i8 + i4 + i1).
>From there it should be trivial to match Haskell IntegerS to Nat.
Am I on the right track here?

-- Oscar
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20101014/34fc9d6a/attachment.html