TypeFamilies vs. etc - TTypeable
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
>higher-order functional programming at the type level).
>instances may indeed be avoided. The library does not use
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
- 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
- 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
More information about the Haskell-prime