TypeFamilies vs. etc - TTypeable

Anthony Clayden anthony_clayden at clear.net.nz
Tue Jun 28 08:07:23 CEST 2011


 <dm-list-haskell-prime at ...> writes:

> 
Thanks David,

For the +1 vote on the word "restraints". Yes, my thinking was that it was 
both sufficiently suggestive and sufficiently separate from "constraints". 
Also 'restrained' has an overtone of civilised and moderate, compared to 
the 'wild west' of overlaps and fundeps.

I'm a bit hesitant to draw any conclusions from my comments, until I've seen 
something from the 'brains trust'. At least nobody's (yet) told me I'm being 
dumb.

Yes, there could be many ways of encoding the type constructors, but that's 
not what I was worried about (nor about the context stack). Let me spell out 
the scenario:
   In my package/module, I declare some data types,
   and encode them with instances for TC_code.
   I import a library/module, which imports ..., which imports ...
   (Or my client combines my package into their project, with other imports.)
   That remote import declares different data types,
   but declares instances for TC_code whose RHS TypeRep are duplicates of mine.
The only way (I can see) to be sure to avoid that is (as you suggest) encode 
the package, module and symbol.

But GHC (and indeed Hugs) has a perfectly workable way to do that already. I 
don't know the internals of it, but I know it's good enough to drive 
overlapping instances *provided the types are grounded*.

My view is that despite all the misgivings, overlaps have been remarkably 
successful and stable considering their poorly-understand theoretical basis, 
and lack of any real work on them for going on a decade. (The HList paper is 
2004, there's since been all sorts of fancy type innovations, including 
families, but all of the HList stuff still works.)

There is more subtlety in Oleg's proposal than I at first understood. He does 
indeed ground all the types by applying constructors to the unit type (), when 
passing to TYPEOF. So Oleg's correct to say "The arguments to StateT ... are 
irrelevant ..." (Combined with all the parentheses for the type-level Succ's, 
his code is beginning to look suspiciously LISP-like ;-)

But unground types were a concern with HList, where you're trying to simulate 
extensible records, and combining data with Higher-level functions a la Object-
oriented style.

Another (possible) example of ungroundedness is the IsFunction type function:
>     instance IsFunction (a -> b) = TTrue     -- a, b not grounded
>     instance IsFunction a | a /~ (_ -> _) = TFalse
>     -- deliberately use `_` placeholder for the args,
>     -- because it's meaningless to ground them

For type inference to work there, we don't need to refine the type beyond its 
outermost type constructor. (And this is one example where currently HList's 
TypeEq doesn't always work for polymorphic functions.)

As another example of Oleg's subtleties, I hadn't realised that you could 
include more than one type constructor for your 'Special instances': Type 
Special is a list (HList-like), not a single type. (Again with each element 
having the constructor grounded on () arguments.)

But the Special instances have to be declared all together. So I don't see 
this as providing any greater flexibility than Closed type classes, or a 
finite number of instances declared with inequality restraints.


AntC


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







More information about the Haskell-prime mailing list