I have implemented type-level TYPEREP (along with a small
Thank you Oleg library for
higher-order functional programming at the type level). Overlapping instances may indeed be avoided. The library does not use functional dependencies either. ........
So this is essentially the approach discussed in the HList paper, translated to a Type Family context. Totally brilliant, and almost impenetrable. If I understand what's going on (big IF), I'm wondering a few things: - You've used type-level NAT to encode the type. What if two different types get encoded as the same NAT? In your MonadState example you've encoded StateT as FOUR ::: NAT, and W as FIVE. What if there's some other module (in a distant import) that also uses FOUR? In general, how do we co-ordinate the encoding of types to avoid duplicates? - Special instances: you say for MonadState' "add more if needed". But can we really do that? The default instance has constructor MState hard coded in the result of function MState'. - Groundedness issues (per Section 9 of the HList paper, 'Reification ...' subsection. The instances of TYPEOF require the type constructor to be grounded; and TYPEOF recurses to reify all the constructor's type arguments. Does this mean all types and arguments have to be fully grounded? Is this really gaining anything over the Type-indexed rows approach you discuss in the HList paper - that is, using instances instance TypeEq x x HTrue instance (b ~ HFalse) => TypeEq x y b -- (using ~ instead of TypeCast) except that it's avoiding fundeps and overlapping instances? That is: is the TYPEOF approach to type equality going to suffer the same issues discussed at the start of section 9 'By chance or by design'? I'm imagining a Haskell' with type functions and a restrained sort of instance overlap: type instance TypeEqF x x = HTrue type instance TypeEqF x y | x /~ y = HFalse (Which is roughly what last month's Haskell-prime discussion talked about, and SPJ picked up on at the start of this TypeFamilies thread.) AntC