[Haskell-cafe] Re: irrefutable patterns for existential types / GADTs

[Conor McBride]

Hi

apfelmus at quantentunnel.de wrote:
> To summarize, the main problem is to get a lazy/online algorithm (the
> problem here falls into the "more haste, less speed" category) while
> staying more type safe.
> @Conor: how does this issue look like in Epigram?
>   

Thanks for asking!

In the current Epigram prototype editor/checker, nothing clever happens.
Apart from anything else, typechecking relies on /partial/ evaluation,
so we can't presume that the only normal forms in a datatype are made
with constructors: they might be expressions which have got stuck.

However, Edwin Brady's prototype compiler delivers code for
run-time-only usage, and here we begin to get paid for working in a
total (once suitably stratified) language. It isn't necessary to perform
constructor discrimination when it's statically known that exactly one
constructor is possible, so those patterns can always be made
irrefutable, with matching replaced by projection. It's not yet obvious
whether this is always, never, predictably sometimes, or unpredictably
sometimes a good idea. However, we'd certainly be able to support an
explicit notation for irrefutable patterns, guaranteed to match whenever
the named subobjects were needed.

So we don't just give that coerce example an irrefutable pattern, we can
erase all run-time trace of equality evidence, and indeed any other data
whose value is completely determined by the indices of its type. If you
don't need to discriminate on it, you don't need to look at it, so you
don't need to keep it.

Even though type-vs-value distinction no longer aligns with the
static-vs-dynamic distinction, you don't get any less run-time
type-erasure. You should actually get more run-time value-erasure!

Online algorithms do look like a good place to try to get some leverage
from this, but we haven't really been in a position to experiment so
far. I'm sure that will change.

All the best

Conor



This message has been checked for viruses but the contents of an attachment
may still contain software viruses, which could damage your computer system:
you are advised to perform your own checks. Email communications with the
University of Nottingham may be monitored as permitted by UK legislation.