Hi apfelmus@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.