TypeFamilies vs. FunctionalDependencies & type-level recursion
Roman Leshchinskiy
rl at cse.unsw.edu.au
Tue May 31 23:45:50 CEST 2011
On 30/05/2011, at 00:55, dm-list-haskell-prime at scs.stanford.edu wrote:
> I'm absolutely not advocating making overlapping instances (or, worse,
> overlapping types) part of Haskell', nor under the impression that the
> committee would ever consider doing so. I'm just pointing out that
> right now OverlappingInstances are the only way to do recursive
> programming at the type level, for the specific reasons I outlined. I
> hope that before FunctionalDependencies or TypeFamilies or any other
> type-level programming becomes part of Haskell', there is a way to
> differentiate base and recursive cases *without* overlapping
> instances.
FWIW, I don't think this is really about type-level recursion. You can do recursive programming with type families:
data Z
data S n
type family Plus m n
type instance Plus Z n = n
type instance Plus (S m) n = S (Plus m n)
It's deciding type equality via overlapping instances that is problematic here. But, as others have pointed out, this is somewhat dodgy anyway. I suppose what you really want is something like this:
data True
data False
type family Equal a b
Where Equal a b ~ True if and only if a and b are known to be the same type and Equal a b ~ False if and only if they are known to be different types. You could, in theory, get this by defining appropriate instances for all type constructors in a program:
type instance Equal Int Int = True
type instance Equal Int [a] = False
type instance Equal [a] Int = False
type instance Equal [a] [b] = Equal a b
...
But that's infeasible, of course. However, nothing prevents a compiler from providing this as a built-in. Arguably, this would be much cleaner than the solution based on fundeps and overlapping instances.
Roman
More information about the Haskell-prime
mailing list