TypeFamilies vs. FunctionalDependencies type-level recursion
I'm not sure if these extensions are still under discussion or if the
topic is dead (wiki pages 5 years old). However, the Haskell' wiki
page for FunctionalDependencies suggests AssociatedTypes is a more
promising approach, yet the AssociatedTypes page misses a major Con
compared to FunctionalDependencies that I think should be there.
One of the more disgusting but also powerful implications of
FunctionalDependencies is that, in conjunction with
OverlappingInstances and UndecidableInstances, you can do recursive
programming at the type level. This has been (ab)used to do some cool
things (e.g., HList, HaskellDB, OOHaskell).
As an example, consider the following simple (key, value) lookup
function that operates at the type level (inspired by HList):
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE OverlappingInstances #-}
{-# LANGUAGE FunctionalDependencies #-}
{-# LANGUAGE UndecidableInstances #-}
data HNil = HNil deriving (Show)
data HCons h t = h :* t deriving (Show)
infixr 2 :*
data A = A deriving (Show)
data B = B deriving (Show)
data C = C deriving (Show)
abc :: HCons (A, Int) (HCons (B, Int) (HCons (C, Int) HNil))
abc = (A, 1) :* (B, 2) :* (C, 3) :* HNil
class HLookup k l v | k l - v where
hLookup :: k - l - v
instance HLookup k (HCons (k, v) l) v where
hLookup _ (h :* t) = snd h
instance (HLookup k l v) = HLookup k (HCons h l) v where
hLookup k (h :* t) = hLookup k t
b :: Int
b = hLookup B abc -- Returns 2
The key to hLookup is that OverlappingInstances selects the most
specific match, thereby breaking the recursion when the requested key
type matches the key of the pair at the head of the list. By
contrast, TypeFamilies cannot permit a function such as hLookup. One
may try something along the lines of:
class HLookup k l where
type HLookupResult k l
hLookup :: k - l - HLookupResult k l
instance HLookup k (HCons (k, v) l) where
type HLookupResult k (HCons (k, v) l) = v
hLookup _ (h :* t) = snd h
instance (HLookup k l) = HLookup k (HCons h l) where
type HLookupResult k (HCons h t) = HLookupResult k t
hLookup k (h :* t) = hLookup k t
But now you have overlapping type synonyms, which pose a safety threat
where the more-specific instance is not in scope. Therefore, Haskell
likely cannot be extended to accept code such as the above.
One possible extension that *would* enable type-level recursive
programming is the ability to constrain by inequality of types. I
noticed GHC is on its way to accepting a ~ b as a constraint that
types a and b are equal. If there were a corresponding a /~ b, then
one might be able to say something like:
instance HLookup k (HCons (k, v) l) where
...
instance (h /~ (k, v), HLookup k l) = HLookup k (HCons h l) where
...
Of course, I have no idea how the compiler could know such constraints
are sufficient to avoid overlapping types. I suspect figuring it out
would be hard given that instance matching happens before context
verification and that the overlapping errors must happen at instance
matching time.
My bigger point is that if the Haskell' committee ever considers
adopting one of these proposals or one intended to supersede them, I
hope there is a way to do recursive type-level programming. A likely
corollary is the need for a mechanism to avoid instance overlap
between recursive and base cases by asserting type inequality in the
recursive case.
David
___
Haskell-prime mailing list
Haskell-prime@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-prime
Re: TypeFamilies vs. FunctionalDependencies type-level recursion
On 29.05.2011 22:59, David Mazieres wrote: But now you have overlapping type synonyms, which pose a safety threat where the more-specific instance is not in scope. Therefore, Haskell likely cannot be extended to accept code such as the above. No it could. Inconsistency arise from fact that it's not guaranted that all instances are known. Such guaranties are possible with closed type families. In such families instances could be added only in the same module with family declaration. Here is simplistic example: data HTrue data HFalse closed type family Equal a b :: * closed type instance a a = HTrue closed type instance a b = HFalse No more instances could be added. So type could be determined unambigously. In type level programming type families often meant to be closed but there is no explicit way to say that and it limit their expressiveness. Also closed type families could help with lack of injectivity. It could be untracktable though. One possible extension that *would* enable type-level recursive programming is the ability to constrain by inequality of types. I noticed GHC is on its way to accepting a ~ b as a constraint that types a and b are equal. If there were a corresponding a /~ b, then one might be able to say something like: instance HLookup k (HCons (k, v) l) where ... instance (h /~ (k, v), HLookup k l) = HLookup k (HCons h l) where ... I can't see how it change things. AFAIR instances selected only by their heads, contexts are not taken into account. Besides type inequality could be easily implemented with closed type families. See code above. Here is contrived example of usage: instance (Equal Thing Int ~ HFalse) = Whatever Thing P.S. Also I have suspicion that version with fundeps will behave badly if more instances are added in another module. ___ Haskell-prime mailing list Haskell-prime@haskell.org http://www.haskell.org/mailman/listinfo/haskell-prime
Re: TypeFamilies vs. FunctionalDependencies type-level recursion
On Sun, May 29, 2011 at 7:59 PM, David Mazieres dm-list-haskell-pr...@scs.stanford.edu wrote: One of the more disgusting but also powerful implications of FunctionalDependencies is that, in conjunction with OverlappingInstances and UndecidableInstances, you can do recursive programming at the type level. This has been (ab)used to do some cool things (e.g., HList, HaskellDB, OOHaskell). It would seem very strange to me if haskell-prime made the choice of fundeps/type families based on the behaviour with OverlappingInstances. I'm under the impression that Overlapping is generally considered one of the more controversial extensions, and on the LanguageQualities wiki page [1] it's explicitly given as an example of something which violates them. So not only is Overlapping not in the language, but I imagine there are many people (myself included) who would like to ensure it stays out. My personal opinion is that if Haskell wants a more complete facility for type-level programming, that should be addressed directly, instead of via creative abuse of the class system and related machinery. Ben [1]: http://hackage.haskell.org/trac/haskell-prime/wiki/LanguageQualities ___ Haskell-prime mailing list Haskell-prime@haskell.org http://www.haskell.org/mailman/listinfo/haskell-prime
Re: TypeFamilies vs. FunctionalDependencies type-level recursion
On Sun, May 29, 2011 at 6:45 PM, Ben Millwood hask...@benmachine.co.uk wrote:
It would seem very strange to me if haskell-prime made the choice of
fundeps/type families based on the behaviour with
OverlappingInstances. I'm under the impression that Overlapping is
generally considered one of the more controversial extensions, and on
the LanguageQualities wiki page [1] it's explicitly given as an
example of something which violates them. So not only is Overlapping
not in the language, but I imagine there are many people (myself
included) who would like to ensure it stays out.
My personal opinion is that if Haskell wants a more complete facility
for type-level programming, that should be addressed directly, instead
of via creative abuse of the class system and related machinery.
It should also be noted: the fact that functional dependencies work
with overlapping instances, while type families don't is not really
inherent in functional dependencies, but is instead related to choices
about how functional dependencies work that differ from how type
families do. And mainly, this is because functional dependencies fail
to incorporate local information, meaning they fail to work
appropriately in various situations (for instance, matching on a GADT
may refine a type, but that new information may not propagate through
a fundep).
In my experience, you can construct examples that should lead to type
soundness issues with fundeps, and only fail because of peculiarities
in fundep handling. But fundeps could (and arguably should, to
interact with GADTs and the like) be reworked to behave 'properly'.
It's just that type families already do.
I can't really recall what example I used in the past, but here's one
off the cuff:
module A where
class C a b | a - b where
instance C a a where
data T a where
CT :: C a b = b - T a
module B where
import A
instance C Int Char where
c :: Char
c = case t of { CT x - x }
So, the question is: what should happen here?
We've created a T Int in a context in which C Int Int, so it wraps an
Int. Then we match in a context in which C Int Char. But the fundep
tells us that there can only be one S such that C Int S. So we have
some choices:
1) Disallow the overlapping instance C Int Char, because it is
incompatible with the C Int Int from the other module. This is what
GHC 7 seems to do.
2) Pretend that there may in fact be more than one instance C Int a,
and so we can't infer what a is in the body of c. I think this is what
GHC used to do, but it means that whether a fundep a - b actually
allows us to determine what b is from knowing a is kind of ad-hoc and
inconsistent.
3) Allow c to type check. This is unsound.
1 is, I think, in line with type families. But it rules out the
computation that fundeps + overlapping can do and type families
cannot.
Also, in an unrelated direction: there are conditions on type families
that can allow some overlapping to be permitted. For instance, if you
simply want a closed type function, like, taking the above as an
example:
type family F a :: * where
instance F Int = Char
instance F a = a
Then this is a sufficient condition for overlapping to be permissible.
And it covers a lot of the use cases for overlapping instances, I
think.
-- Dan
___
Haskell-prime mailing list
Haskell-prime@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-prime
Re: TypeFamilies vs. FunctionalDependencies type-level recursion
Thanks for the responses. I realized after sending the message that it wasn't clear exactly what I was advocating, which is probably more modest that what people are thinking. Mostly I was hoping the AssociatedTypes wiki page could be updated to reflect that AssociatedTypes can't replace FunctionalDependencies. (After reading the FunctionalDependencies page, I converted a bunch of code over to TypeFamilies, thinking this would be more future-proof, only to realize it couldn't work.) I'm not sure what the process is for updating the wiki, as the page is locked down, but mailing haskell-prime seemed like a reasonable start. 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. The fact that TypeFamilies made it somewhat far into the process without a way to do recursion and that the limitation is not even documented on the wiki suggests that the Haskell' committee either thinks people don't care or thinks about the question differently. Either way, the point seemed worth noting somewhere. I don't have any great ideas on supporting recursion, so I suggested a not so great idea in my last email that abused the context. Here's another not so great idea that doesn't abuse the context... The point is just that it's possible to support recursion without overlapping instances: Add an annotation like | x /~ y, ... to instances denoting that the instance cannot be selected unless types x and y are known to be different. So the code from my previous message becomes: data HNil = HNil deriving (Show) data HCons h t = h :* t deriving (Show) infixr 2 :* class HLookup k l where type HLookupResult k l hLookup :: k - l - HLookupResult k l instance HLookup k (HCons (k, v) l) where ... type HLookupResult k (HCons (k, v) l) = v hLookup _ (h :* t) = snd h instance (HLookup k l) = HLookup k (HCons h l) | h /~ (k, v) where -- This is how we avoid overlap ^^^ type HLookupResult k (HCons h t) = HLookupResult k t hLookup k (h :* t) = hLookup k t I'm under no illusions that this specific syntax would fly, but possibly some other proposal will allow the equivalent. David ___ Haskell-prime mailing list Haskell-prime@haskell.org http://www.haskell.org/mailman/listinfo/haskell-prime
Re: TypeFamilies vs. FunctionalDependencies type-level recursion
At Sun, 29 May 2011 19:35:15 -0400, Dan Doel wrote: On Sun, May 29, 2011 at 6:45 PM, Ben Millwood hask...@benmachine.co.uk wrote: 1) Disallow the overlapping instance C Int Char, because it is incompatible with the C Int Int from the other module. This is what GHC 7 seems to do. This seems like the only reasonable option given the meaning of functional dependencies. Also, in an unrelated direction: there are conditions on type families that can allow some overlapping to be permitted. For instance, if you simply want a closed type function, like, taking the above as an example: type family F a :: * where instance F Int = Char instance F a = a Something like this would be good. Though you'd need a corresponding value-level mechanism. Is this part of any pending proposal? I don't suppose there's any way to get GHC to accept such code? I only found one cryptic mention of closed synonym families under a speculative ideas list for type functions. David ___ Haskell-prime mailing list Haskell-prime@haskell.org http://www.haskell.org/mailman/listinfo/haskell-prime
