
27 Jun
2010
27 Jun
'10
9:30 a.m.
On 27/06/2010, at 19:54, Max Bolingbroke wrote:
Q: What is the "mother of all X", where X is some type class? A: It is a data type D such that:
1. There exist total functions:
lift :: X d => d a -> D a lower :: X d => D a -> d a
Are those universally quantified over d? If so, then none of your examples fit this definition. I assume you mean this: lift :: X d => d a -> D d a lower :: X d => D d a -> d a In that case, isn't D just the dictionary for (X d) and a value of type (d a)? I.e., couldn't we always define it as: data D d a where { D :: X d => d a -> D d a } Roman