Core and elaboration [Re: [Agda] --no-pattern-matching]

[Andreas Abel]

On 18.01.2014 01:00, Conor McBride wrote:
> On 17 Jan 2014, at 23:37, Andreas Abel <andreas.abel at ifi.lmu.de> wrote:
>> --no-pattern-matching is an extreme form of chastity, but it should not hard to implement it.

> Indeed. It's not even that hard to implement things which look like
> pattern matching, but aren't. In fact, I recommend it.

You try to make me think here, but it is late, and I give up.  What did 
you mean by your statement?

> Agda remains fundamentally troubled by its failure to separate its
> surface programming language from its (somewhat nebulous) kernel.
> It's in good company, of course, but I really think it's worth trying
> to nail down what is the type theory and what is elaboration.

Agreed.  Some efforts are going on here in the direction of a core language.

However, I'd rather not have eliminators as core, if it can be avoided. 
  Mutually recursive functions defined by case trees with type-based 
termination would be my ideal, but I am aware how far away we are still 
from that sweet spot.

Cheers,
Andreas

-- 
Andreas Abel  <><      Du bist der geliebte Mensch.

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