[Agda] Pie in the sky

[Benja Fallenstein]

Hi Andreas,

On Tue, Sep 21, 2010 at 9:31 AM, Andreas Abel <andreas.abel at ifi.lmu.de> wrote:
> Maybe this discussion can refine your idea...

Yes, that would clearly be good :-)

> Why is it that you require the thing to be named by its type?  Is not it
> more like you want to say that
>
>  bla : Ord Int
>  bla = record ...
>
> should be taken whenever you need something of type "Ord Int" which has not
> been supplied by the user.  So you could mark this declaration by some
> keyword
>
>  instance
>    bla : Ord Int
>    bla = ...
>
> which tells Agda to use bla as he canonical instance for Ord Int.  You could
> then separate instance delaration from definition.
>
>  bla : Ord Int
>  bla = ...
>
>  ...
>
>  instance bla : Ord Int

Technically, this seems not so different from my proposal; IIUC, it's
not the declaration of 'bla', but the declaration of anything of type
"Ord Int" inside the instance keyword, that makes the instance
searcher use this. (I think you agree it would not be a good idea to
use any old thing of type "Ord Int" found in the context; this would
probably be too confusing when there's more than one instance
available.) So when you write

  instance
    bla : Ord Int
    bla = ...

or

  bla : Ord Int
  bla = ...

  instance bla : Ord Int

this seems to be equivalent to writing in my proposal

  bla : Ord Int
  bla = ...

  _ : Ord Int
  _ = bla

However, I agree that using the 'instance' keyword looks clearer than
the blank. On the other hand, it seems annoying to have to come up
with a name for every instance you write -- it seems to me that not
naming (default) instances is a worthy feature of Haskell, because
often enough you can't do much better than "ordInt".

Perhaps it would be better to write

  instance : Ord Int
  instance = ...

(where instance is a keyword), or using Samuel's proposed keyword
slightly differently

  default : Ord Int
  default = ...

Or you could combine both proposals and allow both your declaration of
instance bla = ..., and

  instance
    _ : Ord Int
    _ = ...

But since I expect not naming the instance to be common, I think it
might be better to optimize for that and do the other use case through

  bla : Ord Int
  bla = ...

  instance : Ord Int
  instance = bla

The advantage of both my original _ notation and your version of
'instance' is that it's clearer at a glance that this is special
syntax going on, not just the declaration of a vanilla variable named
'instance.' It would be nice to both have this property, and not
having to name every instance.

> The question is how you export and import such instance declarations and how
> they interact with modules.

Oh wait -- that gives me an idea, how about naming them

  instance Ord Int = ...

which then also allows you to write

  bla : Ord Int
  bla = ...

  instance Ord Int = bla

Then it would be clear that you could write

  open A using (instance Ord Int)
  open B hiding (instance Ord Int)
  open C renaming (instance Monoid String to ltrMonoid; rtlMonoid to
instance Monoid String)

On the user level, this (instance Ord Int) is quite similar to
Samuel's '(Ord Int), though I still think it gives a clearer semantics
if we think of the (instance Ord Int) appearing in the context not as
a name, but as a nameless parameter of type Ord Int.

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

Yes, those were the "deeper waters" alluded to in the last lines of my
original proposal :-)

I suppose we really want something like this, but it's not clear to me
how to do it.

Hmm, I never thought about it precisely this way, but are Haskell type
classes without undecidable instances = Horn clauses with a simple
termination checker? If I'm not just hallucinating this, it seems like
it could be a good choice for Agda.

Ah, I suppose then my simple scheme of just putting nameless things in
the context breaks down -- we'd like to do what Haskell does, checking
that instances don't overlap even if they don't have the same number
of arrows in their type. (I.e., when you give the instance you gave
above, you can't also declare Eq (Prod Int Int).)

> A big question is how smart proof search should be in order to be performant
> enough to be used during type checking.  There is already the Agsy tool, but
> I guess it is not deterministic enough.

Yeah, I think full-on proof search would be too heavyweight for this.
Something closer to Haskell's mechanism seems better.

> Also, if you use proof search in relevant contexts, like seaching for and
> instance of Ord (Vec (List Int) n), you should make sure that there is not
> more than one instance.  For this, proof search must follow a strong
> discipline imposed on the form of instance declarations.

Right.

Thanks,
- Benja (who spent the night fighting the Agda type checker and
managed to win some of the battles...)