TypeFamilies vs. FunctionalDependencies & typelevel recursion
Simon PeytonJones
simonpj at microsoft.com
Fri Jul 29 13:42:15 CEST 2011
Friends
This has been an interesting thread, but I've been on holiday, and been busy bugfixing etc, so my cache is very cold. Moreover, I remember that there was much of it that I wasn't following anyway. It's tricky.
So, let me ask: does anyone (eg Oleg) have concrete proposals on the table for things they'd like GHC to do?
Arising from the thread, two particular things jump out at me. I'm not planning to do anything immediate about either of them.
1. Support for type representations. Oleg showed this:
 I have implemented typelevel TYPEREP (along with a small library for higherorder
 functional programming at the type level). Overlapping instances may indeed be
 avoided. The library does not use functional dependencies either.

 http://okmij.org/ftp/Haskell/TTypeable/
Yesterday, Brent, Stephanie, Dimitrios, Julien and I were talking about better support for type reps too, something like a better Typeable class:
class BetterTypeable a where
typeOf :: Proxy a > BetterTypeRep a
data Proxy a
The "better" part is that
 Both BetterTypeable and Proxy could be polykinded, so we didn't need
Typeable1, Typeable2 etc
 BetterTypeRep is typeindexed (unlike the current TypeRep)
But BetterTypeRep is still a valuelevel thing. You want a typelevel type representation, for reasons I don't yet understand.
In any case, *some* built in support for getting at type reps seems reasonable; the question is exactly what.
2. Support for overlapping type function equations.
There seems no reason in principle to disallow
type instance F where
F Int = Bool
F a = [a]
There is overlap, but it is resolved toptobottom. The only real difficulty with this is how to render it into FC. The only decent way seems to me to be to allow FC axioms to do pattern matching themselves. So the FC rendering might be
ax32 a = case a of
Int > F Int ~ Bool
_ > F a ~ [a]
That is, the axioms become typeindexed. I don't know what complications that would add.
Simon
 Original Message
 From: haskellprimebounces at haskell.org [mailto:haskellprimebounces at haskell.org] On
 Behalf Of oleg at okmij.org
 Sent: 28 July 2011 06:28
 To: anthony_clayden at clear.net.nz
 Cc: mazieresxb9592p9wenhvgjq5vnwdnd4be at temporaryaddress.scs.stanford.edu; haskell
 prime at haskell.org
 Subject: Re: TypeFamilies vs. FunctionalDependencies & typelevel recursion


 Let me see if I understand the different points of view. You advocate
 keeping Overlapping Instances, with changes to instance resolution
 algorithm. I advocate abolishing Overlapping Instances,
 claiming it results in no loss of expressiveness. In my approach, the
 changes in GHC are minor (essentially bug fixing and a matter of
 prettyprinting), not involving the algorithms of instance
 resolution. Incidentally, I have advocated abolishing Overlapping
 Instances in a short presentation at the 2004 Haskell Workshop (almost
 immediately after Ralf's HList talk).

 > Selecting instances based on inequalities is already implemented in
 > GHC and Hugs. (And has been successfully used for over a decade.)
 > You've used it extensively yourself in the HList work, and much other
 > typelevel manipulation (such as IsFunction).

 I'm glad you mentioned Hugs. Indeed, Hugs implements overlapping
 instances, and indeed _some_, simple code using overlapping
 instances work the same way in GHC and Hugs. However, HList in
 full does not work in Hugs; while investigating the matter we have
 found many dark corners of the Overlapping Instances
 implementation in Hugs; Ralf has even found an example where the order of
 the constraints within a type mattered. After that we just abandoned
 Hugs. This fact constructively proves that implementation of
 overlapping instances is tricky; since there is no metatheory, it is
 even hard to tell what is right.

 I don't think Overlapping Instances will be in Haskell' any time soon
 since there are doubts about the soundness. Overlapping
 instances are clearly unsound with type functions. Whether they are
 sound with functional dependencies is not clear, but there are warning
 signs:

 http://www.haskell.org/pipermail/haskellcafe/2010July/080043.html

 Please see the whole discussion on HaskellCafe in July 2010.

 > I think this could be implemented under the new OutsideIn(X)
 > type inference:
 I should point out the need to extend the type inference algorithm
 (and prove that the extension is sound) on your point of view. My
 proposal does not affect the instance resolution algorithm at all.


 > I take it the Northern hemisphere is now on academic summer holidays.
 Generally, yes. I wish I had a holiday though...


 _______________________________________________
 Haskellprime mailing list
 Haskellprime at haskell.org
 http://www.haskell.org/mailman/listinfo/haskellprime
More information about the Haskellprime
mailing list