if a sum type is in a bigger sum, then its summands are in that bigger sum too

pa-ba / compdata

Haskell library implementing "Data Types a la Carte"

http://hackage.haskell.org/package/compdata

Other

89 stars 27 forks source link

if a sum type is in a bigger sum, then its summands are in that bigger sum too #27

Open tscholak opened 5 years ago

tscholak commented 5 years ago

it would be great if compdata was providing these instances:

instance (f :+: g) :<: h => f :<: h where ...

instance (f :+: g) :<: h => g :<: h where ...

I would do it downstream, but :<: is a type alias for (Subsume (ComprEmb (Elem f g)) f g), and ComprEmb (from SubsumeCommon) is not exported.

pa-ba commented 5 years ago

Perhaps I am missing something, but I don't see how to implement this easily. The naive way would require adding two instance declarations for Subsume (corresponding to the two instance declarations you list) that are are overlapping and could lead to non-terminating type checking.

Do you have an implementation in mind?