[Agda] Pie in the sky

[Andreas Abel]

Maybe this discussion can refine your idea...

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

The question is how you export and import such instance declarations  
and how they interact with modules.
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.

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.

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.

Cheers,
Andreas


On Sep 21, 2010, at 7:50 AM, Benja Fallenstein wrote:

> Hi Samuel,
>
> On Tue, Sep 21, 2010 at 7:02 AM, Samuel Gélineau <gelisam at gmail.com>  
> wrote:
>> On 2010-09-20 22:31, Andreas Abel wrote:
>>> As I heard from Ulf, the main reason why it is not in Agda is that  
>>> there is
>>> not a good idea yet how to handle scoping.  Haskell's mistakes  
>>> should not be
>>> repeated.
>>
>> I'm not familiar with those mistakes, but it would be important to
>> make sure that Benja's proposed feature doesn't have similar scoping
>> issues, then.
>
> Yeah.
>
>> And as a matter of fact, I think the proposal does have
>> issues, although those I have noticed are probably quite different
>> from Haskell's.
>>
>> First, it seems that the proposal has a slightly inconsistent naming
>> scheme. Sometimes the special implicit values are given the same name
>> as their type, and sometimes their name is an underscore.
>
> Um! I didn't mean to suggest that the parameter of type Ord Int should
> be named by the string "Ord Int" -- what I tried to say was that it
> should not have a formal name at all, and be accessed through its
> type. I suppose calling them "type-named" parameters didn't help,
> though that's how I think about them. Continuing to write _ for the
> missing names, if I write
>
>    sort : forall {A} -> {Ord A} -> List A -> List A
>    sort xs = ...
>
> then in the body of the sort, the context would be
>
> .A : Set
> _ : Ord .A
> xs : List A
>
> When type inference fails to infer a value of type FOO, it would look
> in the context the innermost entry (_ : FOO), if any, and use that.
>
>> Second, the usage examples clearly show that the implicit values are
>> intended to be listed in the type, but not in the pattern-matching
>> part of function definitions. According to the current agda scoping
>> rules, the implicit value should therefore not be in scope inside the
>> body, and the type checker would thus not be able to look in the
>> current environment to find a value whose name is the same as the  
>> type
>> of an implicit value it failed to solve.
>
> True; my proposal would require the rule to change. My idea is that
> whenever the type signature contains an unnamed parameter, like {Ord
> Int}, and this parameter is not matched on in the pattern (left
> implicit), then it's brought into scope as an unnamed parameter of
> that type.
>
>> And now, here is my attempt at fixing the flaws highlighted above. My
>> version of the proposal is to introduce a new syntax for compound
>> names, say '(Foo bar), where (Foo bar) is some expression which agda
>> evaluates to its normal form. Now also introduce the syntax '{Foo
>> bar}, as a shorthand for {'(Foo bar)}, and the keyword (default).  
>> When
>> (default) is put in a context where a value of type (Foo bar) is
>> expected, '(Foo bar) is looked up in the current environment, causing
>> a compile error if none is found.
>
> Do you mean {Foo bar} should be a shorthand for {'(Foo bar) : Foo
> bar}? Or are you saying that '(Foo bar) must always have type Foo bar?
>
> (Note that {varname} is currently illegal syntax in type signatures,
> i.e. you cannot write
>
> foo : {myfoobar} -> Blah
>
> but only
>
> foo : {myfoobar : Foo bar} -> Blah
>
> or
>
> foo : forall {myfoobar} -> Blah.)
>
>> hoping you like my version of the proposal,
>
> It's closer to what I meant to propose than what you read me as saying
> :-) But having the explicit names seems unnecessarily heavyweight to
> me -- what do you think about my idea now that I've hopefully
> explained it somewhat better?
>
> Thanks,
> - Benja
>

Andreas Abel  <><      Du bist der geliebte Mensch.

Theoretical Computer Science, University of Munich
Oettingenstr. 67, D-80538 Munich, GERMANY

andreas.abel at ifi.lmu.de
http://www2.tcs.ifi.lmu.de/~abel/