[Agda] Pie in the sky

[Alan Jeffrey]

On 09/25/2010 03:32 AM, Andreas Abel wrote:
> On Sep 25, 2010, at 3:38 AM, Alan Jeffrey wrote:
>> On 09/24/2010 11:03 AM, Thorsten Altenkirch wrote:
>>> On 24 Sep 2010, at 15:38, Alan Jeffrey wrote:
>>>> A simple example of why M shouldn't be typechecked at compile time
>>>> is a function with type:
>>>>
>>>>   f : (x y : T) ->   {x==y ? refl : x == y} ->   U
>>>
>>> but we could allow instances of the type for defaults, e.g.
>>>
>>> f : (x y : T) ->   {x==y ? refl : x == x} ->   U
>>>
>>> which are only used if the application matches the instance.
>>
>> We might be able to do this example this way, but I suspect in
>> general we'd want to show the existence of a unifier which allows
>> the default to typecheck.  This sounds pretty hairy to me!
>
> Yeah, this was not a good example. ;-)

OK, you got me.  Replace == by your favourite preorder with more than 
one constructor!

> Because how I'd do it would simply be
>
>     f : (x y : T) ->  {x == y} ->  U
>
> the calling
>
>     f x x {?}
>
> the meta-variable ? is eta-expanded at type x == x to refl, and no
> default-argument trickery is needed.  This kind of eta-expansion is
> implemented in MiniAgda, only I have no metavars there. ;-)
>
> Cheers,
> Andreas
>
> 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/
>

A.