TypeFamilies vs. etc - TTypeable

[dm-list-haskell-prime at scs.stanford.edu]

At Sun, 26 Jun 2011 23:25:31 +1200,
Anthony Clayden wrote:
> 
> 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?

I think the type-level Nats are just an example.  Another way to
encode it would be in binary:

	data Z
	data Bit0 a
	data Bit1 a

	type family NatEq x y :: *
	type instance NatEq Z Z = HTrue
	type instance NatEq (Bit0 a) Z = HFalse
	type instance NatEq (Bit1 a) Z = HFalse
	type instance NatEq Z (Bit0 a) = HFalse
	type instance NatEq Z (Bit1 a) = HFalse
	type instance NatEq (Bit0 a) (Bit1 b) = HFalse
	type instance NatEq (Bit0 a) (Bit0 b) = NatEq a b
	type instance NatEq (Bit1 a) (Bit1 b) = NatEq a b

Then you could encode the package, module, and symbol name as a type.

Except even without UndecidableInstances you'll still easily blow
through GHC's default context stack depth of 21, so that needs to be
increased...

> - 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?

Oleg's TYPEOF type function returns both a code for the constructor,
and a list of types of the arguments.  I think the idea is that both
are ground types even if the type arguments they represent are not.

> 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'?

It is essentially a translation of section 9 from fundeps to type
families, so I would imagine the same limitations apply.  However, I'm
wondering where this is really a problem.  I mean the kind of TYPEOF
is * -> *, so you have to feed it a ground type anyway.

Are there situations where you want to decide equality of non-ground
types, and you can't just translate them to ground types through
appropriate functions returning undefined?  E.g., if you have
something of type m a and m' b and want to know if m ~? m', just run
both values through:

    toUnit :: m a -> m ()
    toUnit _ = undefined

> 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.)

Yes, this is obviously something I would like.  It is a far more
drastic change to the language than what Oleg is suggesting.  All Oleg
needs is auto-derived instances, which could be done by a
pre-processor with no modifications to the core compiler.

However, in most cases such an inequality "restraint" (it's good not
to call it a constraint, as constraints are typically not consulted
for instance selection) would specify what programmers want more
directly and likely lead to more readable code.

David