TypeFamilies vs. FunctionalDependencies & type-level recursion

[José Pedro Magalhães]

Hi David,

2011/6/21 <dm-list-haskell-prime at scs.stanford.edu>

> At Tue, 21 Jun 2011 10:01:24 +0200,
> José Pedro Magalhães wrote:
> >
> >     | One thing you could do to help in this specific case would be to
> use a
> >     | different M1 tag--e.g., M1 S ... for selectors and M1 NS ... for
> >     | fields without selectors (or K1 NS).  I presume you've already
> >     | considered this and/or it's too late to make such a change.  (Or to
> >     | move the distinction up to the constructor with two different
> >     | constructor tags, CR and CN for record and no-record.)
> >
> >     I don't think it's too late to make a change.  The stuff has only
> just
> >     gone in, so it's still very malleable.  There may be other
> considerations,
> >     but legacy code isn't one of them!
> >
> > I suppose that could be changed, yes, but what exactly are we trying to
> solve
> > here? One can already specify different behavior for constructors
> with/without
> > named fields. Are we trying to avoid OverlappingInstances? Then yes, this
> > might help, but I'm not sure this change alone would make all generic
> > programming possible without OverlappingInstances.
>
> Sorry, I wasn't necessarily advocating the change.  This came out of a
> long discussion of UndecidableInstances.  Oleg's TYPEOF approach is
> one way to avoid them (or at least to avoid them in conjunction with
> OverlappingInstances).  Before Oleg posted his examples, Simon asked
> if it might be possible to use the new Generic class in a similar way.
> I was pointing out that no you can't, though the specific example I
> gave could be accommodated by a small change to the Generic interface.
>

Ah, I see. Oleg's TYPEOF encodes only the type arguments to a datatype,
whereas Rep encodes the structure of the datatype. As far as I can tell,
TYPEOF never depends on the right-hand side of the datatype. A simple
example is some datatype with a phantom type, say `data P a = P`. TYPEOF
will encode the `a`, whereas Rep will not.

So now it is very clear to me that you cannot get the TYPEOF if you have the
Rep, in general.


Cheers,
Pedro


>
> David
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.haskell.org/pipermail/haskell-prime/attachments/20110622/5d48f10d/attachment-0001.htm>