Re: [Haskell-cafe] DatatypeContexts / alternative

Am 28.02.21 um 20:00 schrieb Richard Eisenberg:

...

On Feb 28, 2021, at 3:25 AM, Ben Franksen wrote:

What are these other GHC features? Does the paper explain this? Otherwise where can I read more about it?

I think it was data families. But, perhaps more troublesome is the fact that the paper assumes a dependently-typed internal language. Maybe it's possible to do this without dependent types in the internal language, but I'm not sure how to begin to think about that problem.

I see. So this cannot be expressed in, say, System Fc? I wonder... is it possible to pinpoint where System Fc is not sufficiently expressive? Perhaps trying to do so exposes a way to extend System Fc that allows to implement this scheme, ideally as step towards a dependently typed IL w/o going the full way. Sorry if these questions are completely naive! I am not versed enough in type theory to full grasp the formulas in these papers in all detail.

I was about to write that it might be helpful to have a GHC proposal to implement this paper, which would depend on (and provide further motivation for) having dependent types... but I'm not actually sure that would be productive at this point.

Yes, this seems to be of relevance only in the very long run. Cheers Ben