TypeFamilies vs. FunctionalDependencies & type-level recursion

[Simon Peyton-Jones]

Friends

This has been an interesting thread, but I've been on holiday, and been busy bug-fixing 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 type-level TYPEREP (along with a small library for higher-order
| 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 poly-kinded, so we didn't need
	  Typeable1, Typeable2 etc
	- BetterTypeRep is type-indexed (unlike the current TypeRep)

But BetterTypeRep is still a value-level thing.  You want a type-level 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 top-to-bottom.  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 type-indexed.  I don't know what complications that would add.


Simon


| -----Original Message-----
| From: haskell-prime-bounces at haskell.org [mailto:haskell-prime-bounces at haskell.org] On
| Behalf Of oleg at okmij.org
| Sent: 28 July 2011 06:28
| To: anthony_clayden at clear.net.nz
| Cc: mazieres-xb9592p9wenhvgjq5vnwdnd4be at temporary-address.scs.stanford.edu; haskell-
| prime at haskell.org
| Subject: Re: TypeFamilies vs. FunctionalDependencies & type-level 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
| pretty-printing), 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
| > type-level 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 meta-theory, 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/haskell-cafe/2010-July/080043.html
| 
| Please see the whole discussion on Haskell-Cafe 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...
| 
| 
| _______________________________________________
| Haskell-prime mailing list
| Haskell-prime at haskell.org
| http://www.haskell.org/mailman/listinfo/haskell-prime