obsidiansystems / dependent-sum

Dependent sums and supporting typeclasses for comparing and displaying them
54 stars 39 forks source link

Make Some more faithfully imitate a datatype #32

Closed treeowl closed 5 years ago

treeowl commented 5 years ago

As I understand it, the ideal implementation would be

data Some tag = forall x. Some !(tag x)

but winning a newtype-like representation for efficiency. But to imitate this faithfully, matching on the Some constructor needs to force the contents.