TypeFamilies vs. etc - TTypeable

[Anthony Clayden]

Thank you Oleg

>I have implemented type-level TYPEREP (along with a small
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