[Agda] Pie in the sky

[Samuel Gélineau]

On Tue, Sep 21, 2010 at 3:31 AM, Andreas Abel <andreas.abel at ifi.lmu.de> wrote:
> Why is it that you require the thing to be named by its type?

Because users are already naming things by their type, using the
ad-hoc strip-whitespace-and-change-to-lowercase convention. My '(...)
notation gives a canonical name for a value of a given type, which is
useful in the common case when there is only one interesting value of
the given type in the current context.

> Also if you want something like Haskell's type classes, you need to generalize this to
>
>  instance
>     blurp : forall {a} -> Eq a -> Eq b -> Eq (Prod a b)
>     blurp (record ...) (record ...) = record ...
>
> But then, naturally, you need proof search for some fragment of FOL, e.g.
> Horn Clauses, to find the instance
>
>  ... : Eq (Prod Nat Bool)
>
> given you have instances for Eq Nat and Eq Bool.

If supporting type classes requires proof search, then no, I do not
want to support type classes. Let's keep things simple! The
underscore-based mechanism currently allows the user to omit some
parameters. My default-based mechanism allows the user to omit
strictly more parameters, at the cost of naming variables in a
slightly-different but actually quite-similar way to the current
naming convention. Proof search would allow the user to omit even
more, but I don't think we're ready for that yet.

I guess Benja and I have both looked in the sky, but the pie he has
seen is not the same pie as the one I have seen after all...

– Samuel