TypeFamilies vs. etc - TTypeable

Anthony Clayden anthony_clayden at clear.net.nz
Sun Jun 26 13:25:31 CEST 2011

Thank you Oleg

>I have implemented type-level TYPEREP (along with a small
library for
>higher-order functional programming at the type level). 
>instances may indeed be avoided. The library does not use
>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
  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
  and TYPEOF recurses to reify all the constructor's type
  Does this mean all types and arguments have to be fully

Is this really gaining anything over the Type-indexed rows
approach you discuss in the HList paper - that is, using
              instance TypeEq x x HTrue
              instance (b ~ HFalse) => TypeEq x y b   --
(using ~ instead of TypeCast)
 except that it's avoiding fundeps and overlapping
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.)


More information about the Haskell-prime mailing list