[Agda] Pie in the sky

[Andreas Abel]

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

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/