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

[Nils Anders Danielsson]

On 2010-10-12 22:14, Oscar Finnsson wrote:
> 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.

Once a module has been successfully checked its dependencies are cached
in memory. Subsequent reloads should be fast, unless the module itself
takes a lot of time to check (or the number of transitive dependencies
is huge, or time stamp checking is very slow, or…).

It is somewhat annoying that the dependency cache is not updated if an
error is encountered (due to the way the monad transformer stack is set
up). Perhaps we should fix this.

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

\ (λ).

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

The slides discuss a feature of (some version of) Agda 1, which is very
different from Agda 2.

> If there are no type classes: can they be simulated somehow using some
> Agda technique?

Dictionary-passing can be implemented manually.

> 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 hope almost all Agda documentation is listed on this wiki page:

   http://wiki.portal.chalmers.se/agda/pmwiki.php?n=Main.Documentation

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

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

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

I think you are referring to the following (incorrect) rule in Ulf's
tutorial:

   "if there is a unique type correct value for the argument it should be
   dotted"

An argument (or sub-pattern) is dotted if /another/ pattern instantiates
it using unification. Let me try to explain using some examples related
to the following equality type:

   data _≡_ : ℕ → ℕ → Set where
     refl : (n : ℕ) → n ≡ n

   f : (n : ℕ) → n ≡ 42 → Bool
   f n eq = ?

Let us "case-split" the eq variable using the Emacs mode (put the cursor
in the goal, write "eq C-c C-c"). We get the following updated clause:

   f .42 (refl .42) = ?

What happened here? The only way in which n ≡ 42 can be unified with
x ≡ x is if x and n are both instantiated to 42, so we got two dot
patterns. Note that the type of the first pattern is still ℕ, for which
many type correct values exist; it is the type of the /second/ pattern
which forces the first to be 42.

As another example, consider sym:

   sym : (m n : ℕ) → m ≡ n → n ≡ m
   sym m n eq = ?

We cannot replace eq with refl x, because this would not satisfy the
constraints m ≡ x and n ≡ x. Depending on whether we keep m, n or x we
get tree different solutions to these constraints, and this corresponds
to three different ways to dot the patterns:

   sym  m .m (refl .m) = refl m
   sym .n  n (refl .n) = refl n
   sym .x .x (refl  x) = refl x

--
/NAD