[Haskell-cafe] DatatypeContexts / alternative

[Ben Franksen]

Am 28.02.21 um 20:00 schrieb Richard Eisenberg:
>> On Feb 28, 2021, at 3:25 AM, Ben Franksen <ben.franksen at online.de>
>> 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