Re: Functional dependencies can return kinds, type families cannot
On Feb 13, 2014, at 4:28 AM, José Pedro Magalhães j...@cs.uu.nl wrote: The most interesting part here is the functional dependency fs - k, where k is a kind variable! If this is not a bug (and it does seem to work as I expect it to), then could we have type families return kinds too?... Yes, I ran into this a while ago. A function dependency on a kind seems to work remarkably well. Can we have type families that return kinds? No. Well, not yet. Functional dependencies inform type inference but don't produce any evidence in Core -- a dependency is only ever used to eliminate ambiguity. On the other hand, a type family does produce evidence (in the form of a type coercion) in Core, and kind coercions turn out to be challenging. How challenging? See System FC with Explicit Kind Equality, ICFP '13 (http://www.cis.upenn.edu/~eir/papers/2013/fckinds/fckinds-extended.pdf) How does this difference between fundeps and type families manifest itself? Type families work much better with GADTs. I don't have an example to hand, but if you're doing GADT programming, using fundeps won't get you very far. That's because the GADTs use the Core coercions internally... and the fundeps don't produce them. Nevertheless, having done the theory behind a Core language with explicit kind coercions, I'm now in the midst of implementing (on a branch -- don't expect anything soon!) type inference for that Core language. In effect, it would be the resolution of GHC bug #7961 (https://ghc.haskell.org/trac/ghc/ticket/7961), but with fairly far-reaching consequences in the implementation. So, if all goes well, we'll have type families returning kinds at some point in the not-too-distant future. Richard___ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
Re: [Haskell-cafe] Re: Functional dependencies and Peano numbers (and hoogle-bug?)
Thanks for the great feedback. The bijective example was especially interesting. While reading Fun with Type Functions I notices GNum as an interesting alternative to the Num type class but I couldn't find any such package on hackagedb. Do anyone know if there is anything like GNum on hackagedb? On an unrelated note: I hoogled to (i.e. http://haskell.org/hoogle/?hoogle=to) and just got a blank page. Nothing. Nil (not even html.../html). Is this a bug or a feature? :) The reason I hoogled it was because I'm searching for something like explicit casting found in many other languages, something similar to class To f t where to :: f - t instance To a a where to x = x instance (Real a, Fractional b) = To a b where to = realToFrac instance (Read a) = To String (Maybe a) where to = maybeRead -- not from cgi :) so I can write something like (23.2 `to`) :: Maybe Double or ((42 :: Integer) `to`) :: Float Anyone made a module/package that solves this problem already? I cannot be the first that needs generic type safe conversion... . -- Oscar ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Re: Functional dependencies and Peano numbers (and hoogle-bug?)
Oscar Finnsson wrote: Anyone made a module/package that solves this problem already? I cannot be the first that needs generic type safe conversion... . There's a restricted version in logfloat:Data.Numer.RealToFrac[1] which generalizes the Prelude's realToFrac to improve performance and correctness. To do much more than that you'll probably have to use something like Data.Data, Data.Typeable, or similar. Generally speaking, arbitrary casts from one type to another go against Haskell ideology because they don't make a lot of sense. Often times there are multiple intelligible ways to convert between two fixed types, so how can we choose? Things like realToFrac, read, show, etc make sense precisely because they are more restricted and therefore make explicit the semantic intentions of how the conversion should be done. [1] http://hackage.haskell.org/packages/archive/logfloat/0.12.1/doc/html/Data-Number-RealToFrac.html -- Live well, ~wren ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Re: Functional dependencies and Peano numbers
On Sun, Jul 11, 2010 at 12:43:47AM +0200, Jose A. Ortega Ruiz wrote: On Sat, Jul 10 2010, wren ng thornton wrote: [...] Yes, you can add multiple dependencies. The syntax is to use , after the first |. While having eight parameters is surely a desperate need for refactoring, there are times when you'd want multiple dependencies. For example, you can say class F a b | a - b, b - a where... to express a bijective function on types (that is, for every pair of A and B, if you know one of them then you know what the other must be uniquely). I know i should read the relevant articles, but how would one express such a bijection using type families? You would just create two type families, one for each direction of the mapping: type family F1 a :: * type instance F1 Int = Bool type instance F1 ... type family F2 a :: * type instance F2 Bool = Int type instance F2 ... Of course, this is not quite the same thing, since with the MPTC version we are guaranteed to get a bijection, but there is nothing forcing F1 and F2 to have anything to do with one another (for example I could have written type instance F2 Char = Int). But I don't know whether this would make a difference in practice. -Brent ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
[Haskell-cafe] Re: Functional dependencies and Peano numbers
On Sat, Jul 10 2010, wren ng thornton wrote: [...] Yes, you can add multiple dependencies. The syntax is to use , after the first |. While having eight parameters is surely a desperate need for refactoring, there are times when you'd want multiple dependencies. For example, you can say class F a b | a - b, b - a where... to express a bijective function on types (that is, for every pair of A and B, if you know one of them then you know what the other must be uniquely). I know i should read the relevant articles, but how would one express such a bijection using type families? TIA, jao -- You err by thinking simplicity and elegance are mostly cosmetic. Simplicity and elegance are overwhelmingly practical virtues. - William D Clinger, comp.lang.scheme ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
[Haskell-cafe] Re: Functional Dependencies Help
On Apr 30, 6:18 pm, John Creighton johns2...@gmail.com wrote:
On Apr 29, 7:47 am, John Creighton johns2...@gmail.com wrote:
I've been trying to apply some stuff I learned about functional
dependencies, but I run into one of two problems. I either end up with
inconsistent dependencies (OverlappingInstances doesn't seem to
apply) or I end up with infinite recursion. I want to be able to do
simple things like if a is a subset of b and b is a subset of c then a
is a subset of c. If a is a is a subset of b and b is a c then a is a
c.
Before I added the equality functions I had infinite recursion. Once I
put them them in then I have trouble with overlapping instances.
I've been doing some reading and I think the following is an
improvement but I end up hanging the compiler so I can't tell what the
errors are. I'll see if their are any trace options that might be
helpfully for GHC.
So bellow I'll post the latest version of my code but first the errors
which seem very strange to me:
could not deduce (IsSuperSet'
isanimal iseq isanimal iseq1 (a - b - c3) )
from the context (IsSuperSet a b c2,
Typeeq a b iseq1,
TypeEq Animal b isaninmal,
IsSuperSet' isanimal iseq1 a b c3)
arising from a use of 'isSuperSet'' at logicp2.hs:92:25-74
Possible fix:
add (IsSuperSet'
isanimal iseq isanimal iseq1 (a - b - c3)) to context
of the declaration
or add an instance delaration for
(IsSuperSet' isanimal iseq isanimal iseq1 (a - b - c3))
In the expression:
(isSuperSet' (u :: isanimal) (u :: iseq) (a :: a)
(b ::b)) :: c3
In the definition of 'isSuperset':
isSuperset a b
= (isSuperSet' (u :: isanimal) (u :: iseq) (a ::
a) (b :: b))
in the instance delaration for 'IsSuperSet a b c3'
Now what is strange about these errors, is the type signature haskell
is asking me to supply instance declarations for. For instance
add (IsSuperSet'
isanimal iseq isanimal iseq1 (a - b - c3)) to context
of the declaration
Why are the first and the third argument the same. Moreover why do the
third and forth arguments look like types related to my Boolean data
types. I see nothing in my code that could result in Haskell needing
this type signature. Also I'm not entirely sure about the (a - b -
c3). Is this the normal way for Haskell to show the type signature of
functional dependencies. My code is bellow and was compiled on GHCi.
{-# LANGUAGE EmptyDataDecls,
MultiParamTypeClasses,
ScopedTypeVariables,
FunctionalDependencies,
OverlappingInstances,
FlexibleInstances,
UndecidableInstances#-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE FlexibleContexts #-}
data Noun = Noun deriving (Show) --15
data Verb = Verb deriving (Show) --
data Adjactive = Adjactive deriving (Show)
data Animal=Animal deriving (Show)
data Feline=Feline deriving (Show) --20
data Cat = Cat deriving (Show)
data Taby_Cat=Taby_Cat deriving (Show)
data T=T deriving (Show)
data F=F deriving (Show) --25
--data Z=Z
--data S i = S i
--type One = S Z
--type Zero = Z
class Isa a b c | a b-c where isa::a-b-c --30
instance Isa Animal Noun T where isa a b = T --
class Parrent a b| a-b where -- Specific Cases
parrent :: a-b --
instance Parrent Cat Feline where --
parrent a = Feline --40
instance Parrent Feline Animal where --
parrent a= Animal --
class TypeOr a b c|a b-c where
typeOr :: a-b-c
instance TypeOr T T T where
typeOr a b = T --50
instance TypeOr T F T where
typeOr a b = T
instance TypeOr F T T where
typeOr a b = T
instance TypeOr F F T where
typeOr a b = T
class TypeEq' () x y b = TypeEq x y b | x y - b
instance TypeEq' () x y b = TypeEq x y b
class TypeEq' q x y b | q x y - b --60
class TypeEq'' q x y b | q x y - b
instance TypeCast b T = TypeEq' () x x b
instance TypeEq'' q x y b = TypeEq' q x y b
instance TypeEq'' () x y F
-- see http://okmij.org/ftp/Haskell/typecast.html
class TypeCast a b | a - b, b-a where typeCast :: a - b
class TypeCast' t a b | t a - b, t b - a where typeCast' :: t-a-
b
class TypeCast'' t a b | t a - b, t b - a where typeCast'' :: t-a-
b --70
instance TypeCast' () a b = TypeCast a b where typeCast x =
typeCast' () x
instance TypeCast'' t a b = TypeCast' t a b where typeCast' =
typeCast''
instance TypeCast'' () a a where typeCast'' _ x = x
-- overlapping instances are used only for ShowPred
class EqPred a flag | a-flag where {}
-- Used only if the other
-- instances don't apply -- 80
class IsSuperSet a b c | a b - c where -- General Definition
isSuperSet :: a-b-c
[Haskell-cafe] Re: Functional Dependencies Help
On Apr 29, 7:47 am, John Creighton johns2...@gmail.com wrote:
I've been trying to apply some stuff I learned about functional
dependencies, but I run into one of two problems. I either end up with
inconsistent dependencies (OverlappingInstances doesn't seem to
apply) or I end up with infinite recursion. I want to be able to do
simple things like if a is a subset of b and b is a subset of c then a
is a subset of c. If a is a is a subset of b and b is a c then a is a
c.
Before I added the equality functions I had infinite recursion. Once I
put them them in then I have trouble with overlapping instances.
I've been doing some reading and I think the following is an
improvement but I end up hanging the compiler so I can't tell what the
errors are. I'll see if their are any trace options that might be
helpfully for GHC.
{-# LANGUAGE EmptyDataDecls,
MultiParamTypeClasses,
ScopedTypeVariables,
FunctionalDependencies,
FlexibleInstances #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-} --10
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE FlexibleContexts #-}
data Noun = Noun deriving (Show) --15
data Verb = Verb deriving (Show) --
data Adjactive = Adjactive deriving (Show)
data Animal=Animal deriving (Show)
data Feline=Feline deriving (Show) --20
data Cat = Cat deriving (Show)
data Taby_Cat=Taby_Cat deriving (Show)
data T=T deriving (Show)
data F=F deriving (Show) --25
--data Z=Z
--data S i = S i
--type One = S Z
--type Zero = Z
class Isa a b c | a b-c where isa::a-b-c --30
instance Isa Animal Noun T where isa a b = T --
class Parrent a b| a-b where -- Specific Cases
parrent :: a-b --
instance Parrent Cat Feline where --
parrent a = Feline --40
instance Parrent Feline Animal where --
parrent a= Animal --
class TypeOr a b c|a b-c where
typeOr :: a-b-c
instance TypeOr T T T where
typeOr a b = T --50
instance TypeOr T F T where
typeOr a b = T
instance TypeOr F T T where
typeOr a b = T
instance TypeOr F F T where
typeOr a b = T
class TypeEq' () x y b = TypeEq x y b | x y - b
instance TypeEq' () x y b = TypeEq x y b
class TypeEq' q x y b | q x y - b --60
class TypeEq'' q x y b | q x y - b
instance TypeCast b T = TypeEq' () x x b
instance TypeEq'' q x y b = TypeEq' q x y b
instance TypeEq'' () x y F
-- see http://okmij.org/ftp/Haskell/typecast.html
class TypeCast a b | a - b, b-a where typeCast :: a - b
class TypeCast' t a b | t a - b, t b - a where typeCast' :: t-a-
b
class TypeCast'' t a b | t a - b, t b - a where typeCast'' :: t-a-
b --70
instance TypeCast' () a b = TypeCast a b where typeCast x =
typeCast' () x
instance TypeCast'' t a b = TypeCast' t a b where typeCast' =
typeCast''
instance TypeCast'' () a a where typeCast'' _ x = x
-- overlapping instances are used only for ShowPred
class EqPred a flag | a-flag where {}
-- Used only if the other
-- instances don't apply -- 80
class IsSuperSet a b c | a b-c where -- General Definition
isSuperSet :: a-b-c
--instance (TypeEq b Animal T,TypeEq c F T)=IsSuperSet a b c where
--85
-- isSuperSet a b = F --
u=undefined
instance (
TypeEq a b iseq, --90
TypeEq Animal b isaninmal,
IsSuperSet' isaninmal iseq a b c3 --
) =
IsSuperSet a b c3 where --
isSuperSet a b=(isSuperSet' (u::isaninmal) (u::iseq) (a::a)
(b::b))::c3
class IsSuperSet' isanimal iseq a b c| isanimal iseq a b-c where
isSuperSet' :: a-b-c
instance IsSuperSet' isanimal T a b T where
isSuperSet' a b = T
instance (Parrent b d, IsSuperSet a b c)=IsSuperSet' F F a b c where
isSuperSet' a b = (isSuperSet a ((parrent (b::b)::d)))::c
instance IsSuperSet' T F a b F where
isSuperSet' a b = F
class ToBool a where
toBool :: a-Bool
instance ToBool T where
toBool a = True
instance ToBool F where
toBool a = False
myCat=Cat
bla=isSuperSet Animal Cat
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
[Haskell-cafe] Re: Functional dependencies conflict between instance declarations
Never mind, that GHC compiler was again more clever than me, sigh. That's really frustrating about Haskell: the compiler captures so many errors at compile time, that newbies hardly get anything done, it's a constant battle against the errors. But once it compiles, it usually works at runtime :-) This is what I love about Haskell: If it typechecks, it probably does the thing you meant it to. I've never seen any other language like it. It's amazing! Next stop: Coq, where the fight with the type checker is so much more difficult that when the code finally type checks you don't even need to run it at all. Stefan ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
RE: [Haskell-cafe] Re: Functional dependencies conflict between instance declarations
Are you kidding, or has automatic proving of programs evolved that far? Anyway, for my sector, videogames, proving if something works correctly is subjective, it's very hard to check if the gameplay of a game is good enough since that involves human fuzzy judgement ;-) Although this might just be statistics, so can be proven too! Aaarrrggg, soon we're all out of job ;-) Peter -Original Message- From: [EMAIL PROTECTED] [mailto:[EMAIL PROTECTED] On Behalf Of Stefan Monnier Sent: Wednesday, September 12, 2007 7:06 PM To: haskell-cafe@haskell.org Subject: [Haskell-cafe] Re: Functional dependencies conflict between instance declarations Never mind, that GHC compiler was again more clever than me, sigh. That's really frustrating about Haskell: the compiler captures so many errors at compile time, that newbies hardly get anything done, it's a constant battle against the errors. But once it compiles, it usually works at runtime :-) This is what I love about Haskell: If it typechecks, it probably does the thing you meant it to. I've never seen any other language like it. It's amazing! Next stop: Coq, where the fight with the type checker is so much more difficult that when the code finally type checks you don't even need to run it at all. Stefan ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Re: Functional dependencies conflict between instance declarations
[EMAIL PROTECTED] wrote: Are you kidding, or has automatic proving of programs evolved that far? Aaarrrggg, soon we're all out of job ;-) Experts have been proclaiming this since high-level programming was invented many decades ago. We're still waiting. ;-) ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
[Haskell] Re: Functional dependencies and type inference (2)
instance CpsForm t t where This can't be right, can it? In general no: the CPS of a function certainly doesn't fit the above pattern. So, if the source language has abstractions (the language in the original message didn't), we have to add another instance for CpsForm. But any other instance will cause problem because the second type won't be functionally dependent on the first any more. Or do you suggest we remove the functional dependency? Stefan ___ Haskell mailing list Haskell@haskell.org http://www.haskell.org/mailman/listinfo/haskell
[Haskell] Re: Functional dependencies and type inference (2)
Stefan Monnier wrote: instance CpsForm t t where This can't be right, can it? In general no: the CPS of a function certainly doesn't fit the above pattern. So, if the source language has abstractions (the language in the original message didn't), we have to add another instance for CpsForm. Actually I started designing such a general typeful CPS of a language with abstractions, applications (and perhaps even call/cc), but then I ran out of time... ___ Haskell mailing list Haskell@haskell.org http://www.haskell.org/mailman/listinfo/haskell
[Haskell] Re: Functional dependencies and type inference (2)
instance CpsForm t t where This can't be right, can it? After CPS conversion a term of type a - b won't have type a - b but rather something like a * (b - c) - c. Stefan ___ Haskell mailing list Haskell@haskell.org http://www.haskell.org/mailman/listinfo/haskell
[Haskell] Re: Functional dependencies and type inference (2)
Louis-Julien Guillemette wrote:
Say we are using a GADT to represent a simple language of boolean
constants and conditionals,
data Term a where
B:: Bool - Term Bool
Cnd :: Term Bool - Term t - Term t - Term t
and we would like to perform a type-safe CPS conversion over this
language. We encode the relationship between the types in the source
language and those in the CPS-converted language using a class and a
fundep:
Here's the code that seems to do what you wished. Liberty is taken
to extend the language so we can CPS convert more interesting terms.
Here are the tests
term1 = Cnd (Cnd (B True) (B False) (B False)) (B True) (B False)
test1 = shw (cps term1 id)
*CPS test1
Cnd (B True)(Cnd (B False)(B True)(B False))(Cnd (B False)(B True)(B False))
term2 = Cnd (Cmp (Cnd (B True) (I 1) (I 2)) (I 3))
(B True) (Cmp (B True) (B False))
test2 = shw (cps term2 id)
*CPS test2
Cnd (B True)(Cnd (Cmp (I 1)(I 3))(B True)(Cmp (B True)(B False)))
(Cnd (Cmp (I 2)(I 3))(B True)(Cmp (B True)(B False)))
The code:
{-# OPTIONS -fglasgow-exts #-}
{-# OPTIONS -fallow-undecidable-instances #-}
module CPS where
data Term a where
B:: Bool - Term Bool
Cnd :: Term Bool - Term t - Term t - Term t
I:: Int - Term Int
Cmp :: Term t - Term t - Term Bool
-- Note the polymorphic answertype
class CpsForm t cps_t | t - cps_t where
cps :: Term t - (Term cps_t - Term w) - Term w
instance CpsForm t t where
cps (B b) c = c (B b)
cps (I b) c = c (I b)
cps (Cnd p q r) c = cps p (\p' - Cnd p' (cps q c) (cps r c))
cps (Cmp p q) c = cps p (\p' - cps q (\q' - c (Cmp p' q')))
shw:: Term t - String - String
shw (B t) = (B ++) . shows t
shw (I t) = (I ++) . shows t
shw (Cnd p q r) = (Cnd ++)
. (showParen True (shw p))
. (showParen True (shw q))
. (showParen True (shw r))
shw (Cmp p q) = (Cmp ++)
. (showParen True (shw p))
. (showParen True (shw q))
term1 = Cnd (Cnd (B True) (B False) (B False)) (B True) (B False)
test1 = shw (cps term1 id)
term2 = Cnd (Cmp (Cnd (B True) (I 1) (I 2)) (I 3))
(B True) (Cmp (B True) (B False))
test2 = shw (cps term2 id)
___
Haskell mailing list
Haskell@haskell.org
http://www.haskell.org/mailman/listinfo/haskell
RE: Functional Dependencies
| class C a b | a - b | instance C Int Bool | | f :: forall a. C Int a = a - a | f x = x | | GHC rejects the type signature for f, because we can see that 'a' *must | be* Bool, so it's a bit misleading to universally quantify it. | | Ok, maybe this is a reasonable choice. But why does the attached program work? | ghci presents a unique type for the universal quantified function 'eight': | | *Add :t eight | eight :: Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ Zero))) From the instance declaration instance Fib Zero (Succ Zero) we get the improvement rule Fib Zero a == a=(Succ Zero) We get a similar rule from instance Fib (Succ Zero) (Succ Zero) But the instance declaration instance (Fib n fib_n, Fib (Succ n) fib_s_n, Add fib_n fib_s_n sum ) = Fib (Succ (Succ n)) sum Fib Zero a gives only Fib Zero a === exists b. b=a which does nothing useful. So when GHC sees the type signature, it's quite happy. No improvement takes place. If you compile Fib with -ddump-types you'll see it gets the type you specify. HOWEVER, when you say :t eight, GHC does not simply report the type of eight. You can type an arbitrary expression there (e.g. :t (reverse hello)). So GHC typechecks the expression eight. So it instantiates its type, and then tries to solve the constraint (Fib (Succ (Succ...)) n). Now it must use the instance declarations to simplify it, and in doing so that exposes more constraints that do force n to be the type you get. I agree this is desperately confusing, and I'm not saying that GHC is doing the Right Thing here; but I wanted to explain what it is doing. Functional dependencies are very slippery. I do not think their behaviour in GHC is necessarily best, nor is their exact behaviour specified anywhere, but I do think the behaviour is consistent. My current belief is that fundeps are too slippery to be given to programmers at all. They are not a good way to express type-level computation. Perhaps associated types might be a better way to express this stuff (see my home page). Simon ___ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
Re: Functional Dependencies
Am Dienstag, 16. August 2005 19:45 schrieb Iavor Diatchki: Hello, I am not sure what GHC is doing, it certainly seems to be inconsistent. In Hugs both the examples work. In case you are interested, here is how you can get a version that works in both Hugs and GHC (I just modified your code a little): [snip] Introducing all these undefined functions is indeed a nice trick - thanks for this hint! Ciao, Dirk ___ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
Re: Functional Dependencies
Picked up on this late... I have working examples of add etc under
ghc/ghci...
I can't remeber all the issues involved in getting it working, but I can
post the
code for add if its any use?
Keean.
Dirk Reckmann wrote:
Am Donnerstag, 11. August 2005 11:41 schrieb Simon Peyton-Jones:
You raise a vexed question, which has been discussed a lot. Should this
typecheck?
class C a b | a - b
instance C Int Bool
f :: forall a. C Int a = a - a
f x = x
GHC rejects the type signature for f, because we can see that 'a' *must
be* Bool, so it's a bit misleading to universally quantify it.
Ok, maybe this is a reasonable choice. But why does the attached program work?
ghci presents a unique type for the universal quantified function 'eight':
*Add :t eight
eight :: Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ Zero)))
Best regards,
Dirk
Simon
| -Original Message-
| From: [EMAIL PROTECTED]
[mailto:glasgow-haskell-users-
| [EMAIL PROTECTED] On Behalf Of Dirk Reckmann
| Sent: 21 July 2005 10:30
| To: glasgow-haskell-users@haskell.org
| Subject: Functional Dependencies
|
| Hello everybody!
|
| I wanted to have some fun with functional dependencies (see
| http://www.cs.chalmers.se/~hallgren/Papers/wm01.html), and tried some
| examples from this paper as well as some own experiments. The idea is
to use
| the type checker for computations by abuse of type classes with
functional
| dependencies.
|
| The example in the attached file is taken from the above paper. Due to
the
| functional dependencies, I expected the type of seven to be uniquely
| determined to be (Succ (Succ (Succ ...))), i. e. seven, but ghc
(version 6.4)
| gives me following error message:
|
| Add.hs:14:0:
| Couldn't match the rigid variable `a' against `Succ s'
| `a' is bound by the type signature for `seven'
| Expected type: Succ s
| Inferred type: a
| When using functional dependencies to combine
| Add (Succ n) m (Succ s), arising from the instance declaration
at
| Add.hs:11:0
| Add (Succ (Succ (Succ Zero))) (Succ (Succ (Succ (Succ Zero
a,
| arising from the type signature for `seven' at Add.hs:13:0-77
| When generalising the type(s) for `seven'
|
| However, using the definition of Add to define Fibonacci numbers does
work,
| and a similar function declaration can be used to compute numbers by
the type
| checker.
|
| The same definition of Add works in Hugs...
|
| So, is this a bug in ghc, or am I doing something wrong?
|
| Thanks in advance,
| Dirk Reckmann
{-# OPTIONS -fglasgow-exts -fallow-undecidable-instances #-}
module Add where
data Zero
data Succ n
class Add n m s | n m - s
instance Add Zero m m
instance Add n m s = Add (Succ n) m (Succ s)
class Fib n f | n - f
instance Fib Zero (Succ Zero)
instance Fib (Succ Zero) (Succ Zero)
instance (Fib n fib_n,
Fib (Succ n) fib_s_n,
Add fib_n fib_s_n sum
) = Fib (Succ (Succ n)) sum
eight :: Fib (Succ (Succ (Succ (Succ (Succ Zero) n = n
eight = undefined
___
Glasgow-haskell-users mailing list
Glasgow-haskell-users@haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
___
Glasgow-haskell-users mailing list
Glasgow-haskell-users@haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
Re: Functional Dependencies
Hello Keean! Am Dienstag, 16. August 2005 13:48 schrieb Keean Schupke: Picked up on this late... I have working examples of add etc under ghc/ghci... I can't remeber all the issues involved in getting it working, but I can post the code for add if its any use? Yes, that would be nice. I'd like to see 'add' working... However, after each answer to my posting, I get more confused. Simon Peyton-Jones took all of my hope to get it working, because ghc doesn't like universal quantified but uniquely idetified types (at least, this is my understanding of his email). Now you have a working 'add' typelevel program. And the most confusing part for me is, that my fibonacci number program works, even though it makes use of the not working version of add. So, I'm really looking forward to your version! Ciao, Dirk ___ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
Re: Functional Dependencies
Hello,
I am not sure what GHC is doing, it certainly seems to be
inconsistent. In Hugs both the examples work. In case you are
interested, here is how you can get a version that works in
both Hugs and GHC (I just modified your code a little):
{-# OPTIONS -fglasgow-exts -fallow-undecidable-instances #-}
module Add where
data Zero; zero = undefined :: Zero
newtype Succ n = Succ n
class Add n m s | n m - s where
add :: n - m - s
add = undefined
instance Add Zero m m
instance Add n m s = Add (Succ n) m (Succ s)
class Fib n f | n - f where
fib :: n - f
fib = undefined
instance Fib Zero (Succ Zero)
instance Fib (Succ Zero) (Succ Zero)
instance (Fib n fib_n,
Fib (Succ n) fib_s_n,
Add fib_n fib_s_n sum
) = Fib (Succ (Succ n)) sum
eight = fib (Succ (Succ (Succ (Succ (Succ zero)
two = add (Succ zero) (Succ zero)
*Add :t eight
eight :: Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ Zero)))
*Add :t two
two :: Succ (Succ Zero)
-Iavor
On 8/16/05, Dirk Reckmann [EMAIL PROTECTED] wrote:
Hello Keean!
Am Dienstag, 16. August 2005 13:48 schrieb Keean Schupke:
Picked up on this late... I have working examples of add etc under
ghc/ghci...
I can't remeber all the issues involved in getting it working, but I can
post the
code for add if its any use?
Yes, that would be nice. I'd like to see 'add' working... However, after each
answer to my posting, I get more confused. Simon Peyton-Jones took all of my
hope to get it working, because ghc doesn't like universal quantified but
uniquely idetified types (at least, this is my understanding of his email).
Now you have a working 'add' typelevel program. And the most confusing part
for me is, that my fibonacci number program works, even though it makes use
of the not working version of add.
So, I'm really looking forward to your version!
Ciao,
Dirk
___
Glasgow-haskell-users mailing list
Glasgow-haskell-users@haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
___
Glasgow-haskell-users mailing list
Glasgow-haskell-users@haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
Re: Functional Dependencies
Am Donnerstag, 11. August 2005 11:41 schrieb Simon Peyton-Jones:
You raise a vexed question, which has been discussed a lot. Should this
typecheck?
class C a b | a - b
instance C Int Bool
f :: forall a. C Int a = a - a
f x = x
GHC rejects the type signature for f, because we can see that 'a' *must
be* Bool, so it's a bit misleading to universally quantify it.
Ok, maybe this is a reasonable choice. But why does the attached program work?
ghci presents a unique type for the universal quantified function 'eight':
*Add :t eight
eight :: Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ Zero)))
Best regards,
Dirk
Simon
| -Original Message-
| From: [EMAIL PROTECTED]
[mailto:glasgow-haskell-users-
| [EMAIL PROTECTED] On Behalf Of Dirk Reckmann
| Sent: 21 July 2005 10:30
| To: glasgow-haskell-users@haskell.org
| Subject: Functional Dependencies
|
| Hello everybody!
|
| I wanted to have some fun with functional dependencies (see
| http://www.cs.chalmers.se/~hallgren/Papers/wm01.html), and tried some
| examples from this paper as well as some own experiments. The idea is
to use
| the type checker for computations by abuse of type classes with
functional
| dependencies.
|
| The example in the attached file is taken from the above paper. Due to
the
| functional dependencies, I expected the type of seven to be uniquely
| determined to be (Succ (Succ (Succ ...))), i. e. seven, but ghc
(version 6.4)
| gives me following error message:
|
| Add.hs:14:0:
| Couldn't match the rigid variable `a' against `Succ s'
| `a' is bound by the type signature for `seven'
| Expected type: Succ s
| Inferred type: a
| When using functional dependencies to combine
| Add (Succ n) m (Succ s), arising from the instance declaration
at
| Add.hs:11:0
| Add (Succ (Succ (Succ Zero))) (Succ (Succ (Succ (Succ Zero
a,
| arising from the type signature for `seven' at Add.hs:13:0-77
| When generalising the type(s) for `seven'
|
| However, using the definition of Add to define Fibonacci numbers does
work,
| and a similar function declaration can be used to compute numbers by
the type
| checker.
|
| The same definition of Add works in Hugs...
|
| So, is this a bug in ghc, or am I doing something wrong?
|
| Thanks in advance,
| Dirk Reckmann
{-# OPTIONS -fglasgow-exts -fallow-undecidable-instances #-}
module Add where
data Zero
data Succ n
class Add n m s | n m - s
instance Add Zero m m
instance Add n m s = Add (Succ n) m (Succ s)
class Fib n f | n - f
instance Fib Zero (Succ Zero)
instance Fib (Succ Zero) (Succ Zero)
instance (Fib n fib_n,
Fib (Succ n) fib_s_n,
Add fib_n fib_s_n sum
) = Fib (Succ (Succ n)) sum
eight :: Fib (Succ (Succ (Succ (Succ (Succ Zero) n = n
eight = undefined
___
Glasgow-haskell-users mailing list
Glasgow-haskell-users@haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
RE: Functional Dependencies
You raise a vexed question, which has been discussed a lot. Should this typecheck? class C a b | a - b instance C Int Bool f :: forall a. C Int a = a - a f x = x GHC rejects the type signature for f, because we can see that 'a' *must be* Bool, so it's a bit misleading to universally quantify it. Simon | -Original Message- | From: [EMAIL PROTECTED] [mailto:glasgow-haskell-users- | [EMAIL PROTECTED] On Behalf Of Dirk Reckmann | Sent: 21 July 2005 10:30 | To: glasgow-haskell-users@haskell.org | Subject: Functional Dependencies | | Hello everybody! | | I wanted to have some fun with functional dependencies (see | http://www.cs.chalmers.se/~hallgren/Papers/wm01.html), and tried some | examples from this paper as well as some own experiments. The idea is to use | the type checker for computations by abuse of type classes with functional | dependencies. | | The example in the attached file is taken from the above paper. Due to the | functional dependencies, I expected the type of seven to be uniquely | determined to be (Succ (Succ (Succ ...))), i. e. seven, but ghc (version 6.4) | gives me following error message: | | Add.hs:14:0: | Couldn't match the rigid variable `a' against `Succ s' | `a' is bound by the type signature for `seven' | Expected type: Succ s | Inferred type: a | When using functional dependencies to combine | Add (Succ n) m (Succ s), arising from the instance declaration at | Add.hs:11:0 | Add (Succ (Succ (Succ Zero))) (Succ (Succ (Succ (Succ Zero a, | arising from the type signature for `seven' at Add.hs:13:0-77 | When generalising the type(s) for `seven' | | However, using the definition of Add to define Fibonacci numbers does work, | and a similar function declaration can be used to compute numbers by the type | checker. | | The same definition of Add works in Hugs... | | So, is this a bug in ghc, or am I doing something wrong? | | Thanks in advance, | Dirk Reckmann ___ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
Re: Functional dependencies, principal types, and decidable typechecking
Manuel M T Chakravarty wrote: I accept that this is the process by which GHC computes these types, but it does violate the principal types property, doesn't it? The relation Int - () = forall c. Int - c does not hold. I realise that principal types and principal typings are slightly different, but I was wondering if the fact that it has recently been shown that Hindley/Milner does not have principal typings has any meaning here? Keean. ___ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
Re: Functional dependencies, principal types, and decidable type checking
Iavor Diatchki wrote:
Hi,
On Apr 3, 2005 7:33 AM, Manuel M T Chakravarty [EMAIL PROTECTED] wrote:
Assume the following type class declarations with functional
dependencies:
{-# OPTIONS -fglasgow-exts #-}
class C a b c | a b - c where
foo :: (a, b) - c
instance C a a r = C a (b, c) r where
foo (a, (b, c)) = foo (a, a)
Now, in GHCi (version 6.4),
*FDs let bar x = foo ((x, x), (x, x))
*FDs :t bar
bar :: (C (a, a) (a, a) c) = a - c
This seems reasonable.
It is reasonable in so far as it is a valid typing, but Haskell
(including FDs) comes with the promise of type inference determining
principal (as in most general) types.
but GHC is also happy to accept the more general type
bar :: a - c
bar x = foo ((x, x), (x, x))
We know
a - c = (C (a, a) (a, a) c) = a - c
where = is the is more or as general as relation, but due to GHCi's
answer to :t bar, it must also be true that
(C (a, a) (a, a) c) = a - c = a - c
To check whether that relation holds, we need to know the set of
satisfiable instances of the predicate C (a, a) (a, a) c under the
given instance declaration. It seems as if we get infinite inference
trees here.
It seems that GHC 6.4 has a new feature where it is creating
recursive dictionaries (which is sometimes useful). Here is a
simpler example of the same behavior:
{-# OPTIONS -fglasgow-exts -fallow-undecidable-instances #-}
class T a where t :: a
instance T a = T a where t = t
f :: Int
f = t
GHC accepts this which means that it managed to discharge the
constraint T Int, and the only way it could have done this is by
creating a recursive (in this case bottom) dicitionary.
Yes, *but* you have given GHC -fallow-undecidable-instances!! My
examples doesn't require that.
*FDs let bar x = foo ((x::Int, x), (x, x))
*FDs :t bar
bar :: Int - ()
This looks like a bug to me.
This only happens when the functional dependency a b - c is used in
the class declaration. I think what is happening is that the type
variable that was to the right of the error is zonked (in error) after
type checking.
I think that if an implementation creates recursive dictionaries it
may be nice to have some sort of a progress check to avoid creating
completely undefined dictionaries. I suspect implementing such a
thing may be tricky though.
I am actually a bit worried about the type theory of this all.
Recursive dictionaries sounds like a cool idea, but what does it mean in
terms of typing derivations? Moreover, how does that combine with
improving substitutions, such as those used in the implementation of
functional dependencies?
Manuel
___
Glasgow-haskell-users mailing list
Glasgow-haskell-users@haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
RE: Functional dependencies, principal types, and decidable typechecking
Manuel
Your short program tickles a lot of different questions. Here's an
explanation.
Simon
| Assume the following type class declarations with functional
| dependencies:
Actually much of the behaviour you see happens without fundeps.
| {-# OPTIONS -fglasgow-exts #-}
|
| class C a b c | a b - c where
| foo :: (a, b) - c
|
| instance C a a r = C a (b, c) r where
|foo (a, (b, c)) = foo (a, a)
You are already on dodgy ground here, because the instance decl doesn't
guarantee that the bit before the = is smaller than the bit after the
=. E.g. context reduction could go:
C (Int,Int) (Bool, Bool) r
-- C (Int,Int) (Int,Int) r
-- C (Int,Int) (Int,Int) r
So [Point 1]: GHC should require -fallow-undecidable-instances if you
use repeated type variables before the =.
| Now, in GHCi (version 6.4),
|
| *FDs let bar x = foo ((x, x), (x, x))
| *FDs :t bar
| bar :: (C (a, a) (a, a) c) = a - c
|
| but GHC is also happy to accept the more general type
|
| bar :: a - c
| bar x = foo ((x, x), (x, x))
There are two separate things going on here
[Point 2] GHC postpones context reduction until it's forced to do it
(except if a single step will eliminate the dictionary altogether).
Example:
data T a = T a
instance Eq (T a)
bar x = [T x] == []
GHC will *infer* bar :: Eq [T a] = a - Bool, but it will happily
*check*
bar :: a - Bool
bar x = [T x] == []
The reason for this lazy context reduction is overlapping instances; in
principle there might be more instances for Eq [T a] at bar's call site.
But now I look at it again, I think it would be OK to postpone context
reduction only if there actually were overlapping instances (right here
at bar's defn). That might be a good idea because it'd give less
confusing types perhaps.
However, note that the two types are indeed equivalent -- both are more
general than the other. It's like saying (Eq Int = t) = t,
and vice versa.
[Point 3] As Iavor notes, yes, GHC is building recursive dictionaries.
Suppose GHC is trying to find evidence for constraint C from a set of
constraints (with evidence provided) D. Suppose it finds an instance
decl D' = C which matches C. Then it tries to prove the constraints
D'. The new bit is that it adds C to D before trying to prove D'.
That's all!
This is Jolly Useful sometimes. (See John Hughes's paper about
restricted type synonyms for example.) It's a bit like infinite data
structures. ML doesn't let you build them, so there's a static error.
Haskell does, and that is sometimes just what you want; and sometimes
gives you runtime divergence (e.g. take the length of an infinite list).
In the same way, this recursive-dictionary thing is sometimes just what
you want; but sometimes gives you runtime divergence instead of a static
error.
| Again, in GHCi,
|
| *FDs let bar x = foo ((x::Int, x), (x, x))
| *FDs :t bar
| bar :: Int - ()
|
| (which by itself is bizarre)
This is the first time when the functional dependency plays a role.
From bar's right-hand-side we get the constraint (C (Int,Int) (Int,Int)
c), and the type (Int - c). Now GHC tries to decide what to quantify
over. Shall we quantify over c? Well, no. GHC never quantifies over
type variables that are free in the environment (of course) OR are fixed
by functional dependencies from type variables free in the environment.
In this case the functional dependencies tell us that since (Int,Int) is
obviously completely fixed, then there's no point in quantifying over c.
So bar is not quantified. The constraint (C (Int,Int) (Int,Int) c) is
satisfied via the recursive dictionary thing, leaving 'c' completely
unconstrained. So GHC chooses c to be (), because it doesn't like to
leave programs with completely free type variables.
| but it also accepts
|
| bar :: Int - c
| bar x = foo ((x::Int, x), (x, x))
Here you are *telling* GHC what to quantify over, so the inference of
what to quantify doesn't happen.
___
Glasgow-haskell-users mailing list
Glasgow-haskell-users@haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
RE: Functional dependencies, principal types, and decidable typechecking
Simon Peyton-Jones wrote:
| {-# OPTIONS -fglasgow-exts #-}
|
| class C a b c | a b - c where
| foo :: (a, b) - c
|
| instance C a a r = C a (b, c) r where
|foo (a, (b, c)) = foo (a, a)
You are already on dodgy ground here, because the instance decl doesn't
guarantee that the bit before the = is smaller than the bit after the
=. E.g. context reduction could go:
C (Int,Int) (Bool, Bool) r
-- C (Int,Int) (Int,Int) r
-- C (Int,Int) (Int,Int) r
So [Point 1]: GHC should require -fallow-undecidable-instances if you
use repeated type variables before the =.
Yes, I think that would be a good idea.
| Now, in GHCi (version 6.4),
|
| *FDs let bar x = foo ((x, x), (x, x))
| *FDs :t bar
| bar :: (C (a, a) (a, a) c) = a - c
|
| but GHC is also happy to accept the more general type
|
| bar :: a - c
| bar x = foo ((x, x), (x, x))
There are two separate things going on here
[Point 2] GHC postpones context reduction until it's forced to do it
(except if a single step will eliminate the dictionary altogether).
Example:
data T a = T a
instance Eq (T a)
bar x = [T x] == []
GHC will *infer* bar :: Eq [T a] = a - Bool, but it will happily
*check*
bar :: a - Bool
bar x = [T x] == []
The reason for this lazy context reduction is overlapping instances; in
principle there might be more instances for Eq [T a] at bar's call site.
But now I look at it again, I think it would be OK to postpone context
reduction only if there actually were overlapping instances (right here
at bar's defn). That might be a good idea because it'd give less
confusing types perhaps.
However, note that the two types are indeed equivalent -- both are more
general than the other. It's like saying (Eq Int = t) = t,
and vice versa.
Semantically, I understand that the constraint C ((x, x), (x, x) a)
does not constrain the two type variables x and a (and hence, the
two types are equivalent), but I don't see how you can derive that with
the constraint entailment rules
\theta \in P
P ||- \theta
P ||- forall a.\theta
-
P || [t/a]\theta
P || p = \phi P ||- p
P ||- \phi
which I thought are those underlying GHC's type system.
| Again, in GHCi,
|
| *FDs let bar x = foo ((x::Int, x), (x, x))
| *FDs :t bar
| bar :: Int - ()
|
| (which by itself is bizarre)
This is the first time when the functional dependency plays a role.
From bar's right-hand-side we get the constraint (C (Int,Int) (Int,Int)
c), and the type (Int - c). Now GHC tries to decide what to quantify
over. Shall we quantify over c? Well, no. GHC never quantifies over
type variables that are free in the environment (of course) OR are fixed
by functional dependencies from type variables free in the environment.
In this case the functional dependencies tell us that since (Int,Int) is
obviously completely fixed, then there's no point in quantifying over c.
So bar is not quantified. The constraint (C (Int,Int) (Int,Int) c) is
satisfied via the recursive dictionary thing, leaving 'c' completely
unconstrained. So GHC chooses c to be (), because it doesn't like to
leave programs with completely free type variables.
| but it also accepts
|
| bar :: Int - c
| bar x = foo ((x::Int, x), (x, x))
Here you are *telling* GHC what to quantify over, so the inference of
what to quantify doesn't happen.
I accept that this is the process by which GHC computes these types, but
it does violate the principal types property, doesn't it? The relation
Int - () = forall c. Int - c
does not hold.
Summary
~~~
So it seems to me that
* MPTCs with recursive dictionary construction seem to require a
semantic model of subsumption (as the normal constraint entailment rules
would lead to infinite trees).
* MPTCs with recursive dictionary construction and FDs break principal
types.
I guess that's all ok provided GHC enforces the use of
-fallow-undecidable-instances for any instances that need recursive
dictionaries.
Manuel
___
Glasgow-haskell-users mailing list
Glasgow-haskell-users@haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
Re: Functional dependencies, principal types, and decidable type checking
Hi,
On Apr 3, 2005 7:33 AM, Manuel M T Chakravarty [EMAIL PROTECTED] wrote:
Assume the following type class declarations with functional
dependencies:
{-# OPTIONS -fglasgow-exts #-}
class C a b c | a b - c where
foo :: (a, b) - c
instance C a a r = C a (b, c) r where
foo (a, (b, c)) = foo (a, a)
Now, in GHCi (version 6.4),
*FDs let bar x = foo ((x, x), (x, x))
*FDs :t bar
bar :: (C (a, a) (a, a) c) = a - c
This seems reasonable.
but GHC is also happy to accept the more general type
bar :: a - c
bar x = foo ((x, x), (x, x))
It seems that GHC 6.4 has a new feature where it is creating
recursive dictionaries (which is sometimes useful). Here is a
simpler example of the same behavior:
{-# OPTIONS -fglasgow-exts -fallow-undecidable-instances #-}
class T a where t :: a
instance T a = T a where t = t
f :: Int
f = t
GHC accepts this which means that it managed to discharge the
constraint T Int, and the only way it could have done this is by
creating a recursive (in this case bottom) dicitionary.
*FDs let bar x = foo ((x::Int, x), (x, x))
*FDs :t bar
bar :: Int - ()
This looks like a bug to me.
For those who expected GHC to diverge during type checking with the
above class declaration, console yourself by knowing that Hugs (Feb'05)
does diverge...well, it invokes the emergency break:
I think this is what GHC used to do, and indeed seems quite
reasonable. I guess one could be more lazy in the context reduction
(like GHC did in the first example), and only diverge if the function
is actually used.
I think that if an implementation creates recursive dictionaries it
may be nice to have some sort of a progress check to avoid creating
completely undefined dictionaries. I suspect implementing such a
thing may be tricky though.
-Iavor
___
Glasgow-haskell-users mailing list
Glasgow-haskell-users@haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
[Haskell] Re: Functional dependencies interfere with generalization
I'm sorry to open an old wound. I've just had an insight for
a clarification.
On Nov 26, 2003 Ken Shan wrote:
Consider the following code, which uses type classes with functional
dependencies:
{-# OPTIONS -fglasgow-exts #-}
module Foo where
class R a b | a - b where r :: a - b
-- 1
rr :: (R a b1, R a b2) = a - (b1, b2)
rr a = (r a, r a)
-- 2
data RAB a = RAB (forall b. (R a b) = (a, b))
mkRAB :: (R a b) = a - b - RAB a
mkRAB a b = RAB (a, b)
Neither 1 nor 2 passes the type-checker (GHC 6.0.1). The error messages
are similar:
Inferred type is less polymorphic than expected
Quantified type variable `b2' is unified with another
quantified type variable
When trying to generalise the type inferred for `rr'
Signature type: forall a b1 b2.
(R a b1, R a b2) =
a - (b1, b2)
Type to generalise: a - (b1, b1)
In both cases, the compiler is failing to make use of functional
dependencies information that it has at its disposal. Specifically,
it seems to me that, if two type variables b1 and b2 have been unified
due to functional dependencies, making two constraints in the context
identical, then the inner constraint (inner with respect to the scope
of quantified type variables) should be ignored.
Regarding the function rr, I'm afraid I'm compelled to side with the
typechecker. It appears that the typechecker does make use of the
functional dependencies to reject the code because the user has
specified too general a signature. Exactly the _same_ error occurs in
the following code
ab:: a - Maybe a
ab = Just
rrr:: a - (Maybe a, Maybe a1)
rrr a = (ab a, ab a)
Inferred type is less polymorphic than expected
Quantified type variable `a1' is unified with another
quantified type variable `a'
When trying to generalise the type inferred for `rrr'
Signature type: forall a a1. a - (Maybe a, Maybe a1)
Type to generalise: a1 - (Maybe a1, Maybe a1)
When checking the type signature for `rrr'
When generalising the type(s) for `rrr'
Error messages are identical.
Because ab is a function rather than a method, there trivially is a
functional dependency between the function's argument and its result.
Furthermore, exactly the same error occurs in
:: a - b
x = x
Inferred type is less polymorphic than expected
Quantified type variable `b' is unified with
another quantified type variable `a'
When trying to generalise the type inferred for `'
Signature type: forall a b. a - b
Type to generalise: b - b
When checking the type signature for `'
When generalising the type(s) for `'
Regarding the original function rr, the best solution seems to be to
let the compiler figure out its type. It seems in these circumstances
the most general type exists -- and thus the compiler can figure it
out.
Now, regarding function mkRAB. It seems there is a simple solution:
data RAB a = RAB (forall b. (R a b) = (a, b))
mkRAB a = RAB (a, r a)
Indeed, the class R a b promised that there is a function 'r' such
that given a value of type 'a' can produce a value of type 'b'. So, we
can make use of such a function.
One can object: in a value of a type RAB (forall b. (R a b) = (a, b)),
the types of two components of a pair `(a, b)' must be related by the
relation R a b. The values can in principle be arbitrary. What if one
wishes to create a value RAB (x,z) such that the value z has the type of
(r x) but is not equal to (r x)? Well, there is an underhanded way to
help that.
class R a b | a - b where
r :: a - b
r1 :: a - Integer - b
that is, we define an additional method that takes an integer and
somehow makes the value of a type 'b'. We may imagine an Array(s) of all
possible values of type 'b' (specialized for those types 'b' for which
there are instances of the class R) and the method r1 merely uses its
second argument to select from that array. In any case, Goedel showed
that quite many pleasant and unpleasant things can be encoded in
integers. The first argument of r1 is merely a window dressing to
make the typechecker happy.
Thus we can define
mkRAB' a b = RAB (a, r1 a b)
To make the code more concrete, we introduce two instances
instance R Int Char where {r = toEnum; r1 _ = toEnum . fromInteger}
instance R Float (Maybe Float) where
r = Just
r1 _ 1 = Nothing
r1 _ n = Just (fromRational $ toRational (n-1) / (2^(128+1)))
In the second instances, we take advantage of the existence of an
injection from IEEE floating-point numbers to integers.
We can try evaluating mkRAB 65, mkRAB' 65 66, mkRAB' (1.0::Float)
0, etc. -- and everything works.
Building RAB values is not enough -- we should be able to use
them. For example, we should be
Re: Functional dependencies interfere with generalization
On Wed, 26 Nov 2003, Ken Shan wrote:
Hello,
Consider the following code, which uses type classes with functional
dependencies:
{-# OPTIONS -fglasgow-exts #-}
module Foo where
class R a b | a - b where r :: a - b
-- 1
rr :: (R a b1, R a b2) = a - (b1, b2)
rr a = (r a, r a)
-- 2
data RAB a = RAB (forall b. (R a b) = (a, b))
mkRAB :: (R a b) = a - b - RAB a
mkRAB a b = RAB (a, b)
Neither 1 nor 2 passes the type-checker (GHC 6.0.1). The error messages
are similar:
I agree that the typechecker could handle this better, but I don't see why
you should need types like this. You should be able to use
rr :: (R a b) = a - (b,b)
and
data RAB a = forall b. (R a b) = RAB (a,b)
equally well, and these typecheck.
I think the root of the problem is the foralls. The typechecker doesn't
realize that there is only one possible choice for thse universally
quantified values based on the functional dependencies. For rr it
complains because you can't allow every b2, just b2 = b1, not realizing
that that is already implied by the class constraints. Similarly for RAB
it complains because the pair you give it is obviously not unviersally
polymorphic in b, not realizing that there is only one choice for b
consistent with the class constraints. Compare this code:
class R a b where r :: a - b
rr :: (R a b1, R a b2) = a - (b1, b2)
rr x = let rx = r x in (rx, rx)
and
data P a = P (forall b. (a,b))
Off the top of a my head, the solution to this problem would probably be
something like ignoring foralls on a type variable that is determined by
fundeps, but I think the type system would need some sort of new
quantifier or binding construct to introduce a new type variable that is
completely determined by its class constraints. Something like forall a .
constrained b. (R a b) = a - (b, b). A forall binding a variable
determined by fundeps could be reduced to a constrained binding, which
would be allowed to do things like unify with other type variables.
I'm not sure anything really needs to be done. I think you can always
type these examples by unifying the reduntant type variables in a
signature by hand, and by using existentially quantified data types
rather than universally quantified ones. Do you have examples that
can't be fixed like this?
Brandon
Inferred type is less polymorphic than expected
Quantified type variable `b2' is unified with another quantified type
variable `b1'
When trying to generalise the type inferred for `rr'
Signature type: forall a b1 b2.
(R a b1, R a b2) =
a - (b1, b2)
Type to generalise: a - (b1, b1)
When checking the type signature for `rr'
When generalising the type(s) for `rr'
Inferred type is less polymorphic than expected
Quantified type variable `b' escapes
It is mentioned in the environment:
b :: b (bound at Foo.hs:17)
In the first argument of `RAB', namely `(a, b)'
In the definition of `mkRAB': mkRAB a b = RAB (a, b)
In both cases, the compiler is failing to make use of functional
dependencies information that it has at its disposal. Specifically,
it seems to me that, if two type variables b1 and b2 have been unified
due to functional dependencies, making two constraints in the context
identical, then the inner constraint (inner with respect to the scope
of quantified type variables) should be ignored.
Is there a technical reason why the type checker should reject the code
above? Would it be possible to at least automatically define a function
like
equal :: forall f a b1 b1. (R a b1, R a b2) = f b1 - f b2
for every functional dependency, with which I would be able to persuade
the type checker to generalize (Baars and Swierstra, ICFP 2002)? I
suppose I can use unsafeCoerce to manually define such a function... is
that a bad idea for some reason I don't see?
Thank you,
Ken
--
Edit this signature at http://www.digitas.harvard.edu/cgi-bin/ken/sig
Tax the rich!
new journal Physical Biology: http://physbio.iop.org/
What if All Chemists Went on Strike? (science fiction):
http://www.iupac.org/publications/ci/2003/2506/iw3_letters.html
___
Haskell mailing list
[EMAIL PROTECTED]
http://www.haskell.org/mailman/listinfo/haskell
Re: Functional dependencies interfere with generalization
On 2003-11-27T07:51:37-0800, Brandon Michael Moore wrote:
I agree that the typechecker could handle this better, but I don't see why
you should need types like this. You should be able to use
rr :: (R a b) = a - (b,b)
and
data RAB a = forall b. (R a b) = RAB (a,b)
equally well, and these typecheck.
[...]
I'm not sure anything really needs to be done. I think you can always
type these examples by unifying the reduntant type variables in a
signature by hand, and by using existentially quantified data types
rather than universally quantified ones. Do you have examples that
can't be fixed like this?
Thanks for indicating that I am not out of my mind! Unfortunately,
when I try to use an existential type for RAB as you do above, I run
into problems later when unpacking the value. Essentially, I need the
type system to be smart at either universal introduction or existential
elimination. For example, I can't write:
useRAB :: (Eq b, R a b) = RAB a - b - Bool
useRAB (RAB (a, b1)) b2 = b1 == b2
The compiler makes two complaints:
Could not deduce (Eq b) from the context (R a b)
arising from use of `=='
Probable fix:
Add (Eq b) to the existential context of a data constructor
In the definition of `useRAB': useRAB (RAB (a, b1)) b2 = b1 == b2
Inferred type is less polymorphic than expected
Quantified type variable `b' escapes
When checking an existential match that binds
b1 :: b
and whose type is RAB a - b1 - Bool
In the definition of `useRAB': useRAB (RAB (a, b1)) b2 = b1 == b2
The first complaint is that it doesn't know that the b from within the
RAB is an instance of Eq. The second complaint is that it doesn't
know that the b from within the RAB is the same as the one from
outside.
The first complaint seems to be due to failing to infer Eq b1 from
Eq b, R a b, R a b1.
This seems to me like a matter of simply unifying b with b1, but perhaps
I am missing something. As for the second complaint:
I think the root of the problem is the foralls. [...]
Right...
Off the top of a my head, the solution to this problem would probably be
something like ignoring foralls on a type variable that is determined by
fundeps, but I think the type system would need some sort of new
quantifier or binding construct to introduce a new type variable that is
completely determined by its class constraints. Something like forall a .
constrained b. (R a b) = a - (b, b). A forall binding a variable
determined by fundeps could be reduced to a constrained binding, which
would be allowed to do things like unify with other type variables.
Looking at section 6.4 (generalizing inferred types) of Mark Jones's
ESOP 2000 paper (http://www.cse.ogi.edu/~mpj/pubs/fundeps.html), I have
another possible solution that doesn't involve a new kind of quantifier
or binding construct. Jones says that
In a standard Hindley-Milner type system, principal types are
computed using a process of generalization. Given an inferred
but unquantified type P=t, we would normally just calculate the
set of type variables T = TV(P=t), over which we might want to
quantify, and the set of variables V = TV(A) that are fixed in the
current assumptions A, and then quantify over any variables in
the difference, T\V. In the presence of functional dependencies,
however, we must be a little more careful: a variable a that appears
in T but not in V may still need to be treated as a fixed variable
if it is determined by V. To account for this, we should only
quantify over the variables in T\V+.
(Here V+ is the set of all type variables uniquely determined by the
type variables in V via functional dependencies.) Contrary to this
paragraph, I think we can actually be -less- careful in the presence
of functional dependencies: we can quantify over any variable v in T,
even if v also appears in V, as long as v is determined by V\{v} via
functional dependencies, by renaming v to some fresh v'.
Unfortunately, this procedure must be guided by type annotations if it
is to work deterministically (i.e., giving rise to principal types).
For example:
class Q a c | a - c
class R b c | b - c
data QAC a = QAC (forall c. (Q a c) = (a, c))
data RBC b = RBC (forall c. (R b c) = (b, c))
mk2 :: (Q a c, R b c) = a - b - c - (QAC a, RBC b)
mk2 a b c = (QAC (a, c), RBC (b, c))
-- or equivalently --
mk2 a b c = let c' = c in (QAC (a, c'), RBC (b, c'))
Here the type of c aka c' needs to be generalized to
forall c'. (Q a c') = c'
on one hand, and
forall c'. (R b c') = c'
on the other. Both type-schemes are valid semantically, but they are
not comparable -- neither subsumes the other. I would be quite content
with a type-checker that uses local type inference (in this case, the
definition of QAC and RBC) to decide how to generalize.
I've also just discovered Simplifying and Improving Qualified Types
RE: Functional dependencies and Constructor Classes
Mark P Jones writes: | The issue I want to raise is whether constructor classes are | redundant in the presence of FDs No, they are not comparable. Allow me to make the following bold claim. Assume we are given a program that uses the Haskell functor class as in class Functor f where fmap :: (a-b)-(f a-f b) We translate such a program by using class Fmap a b fa fb | a fb - b fa, b fa - a fb, fa fb - a b where fmap :: (a-b)-(fa - fb) instead. Instances are translated in the obvious way. Then, if the original program is typable, so will be the translated program, meaning is preserved. Your fds version of the Functor class is also incomparable with the ccs version; the former will allow an expression like (map id 'a') Yes, because FD's are not expressive enough to specify the form of improvement we need. Consider module Fmap where class Fmap a b fa fb | a fb - b fa, b fa - a fb, fa fb - a b where fmap2 :: (a-b)-(fa - fb) -- identity functor instance Fmap a a a a where fmap2 h = h e = fmap2 id 'a' yields Type checking ERROR Fmap2.hs:17 - Unresolved top-level overloading *** Binding : e *** Outstanding context : Fmap c c Char b though we would like to improve this type to Fmap Char Char Char Char where c=Char and b=Char I believe the same is true in this case. Ccs and fds address different problems. They are complementary tools, each with their own strengths and weaknesses. I believe that a refined form of fds is able to encode Ccs. Give me some time to provide more evidence for my unsupported claims. Martin ___ Haskell mailing list [EMAIL PROTECTED] http://www.haskell.org/mailman/listinfo/haskell
Re: Functional dependencies and Constructor Classes
Martin Sulzmann [EMAIL PROTECTED] writes: Yoann Padioleau writes: nevertheless i found constructor class more elegant for many problems. Your solution is less elegant that the one using constructor classes. Yes, the current presentation of constructor classes might be easier to comprehend. I found too that type error messages of class using functionnal depedencies are not easy to read. There is often ambiguity in code that are not easy to solver. this problem does not appear with constructor classes. Well, that's the point of my encoding of functors using FD's. No ambiguities will arise! The issue I want to raise is whether constructor classes are redundant in the presence of FDs (yes, yes, we still might want to stick to the constructor class representation, but that's a different issue). Oh, sorry, i misinterpret what you wanted to say. Martin -- Yoann Padioleau, INSA de Rennes, France, Opinions expressed here are only mine. Je n'écris qu'à titre personnel. ** Get Free. Be Smart. Simply use Linux and Free Software. ** ___ Haskell mailing list [EMAIL PROTECTED] http://www.haskell.org/mailman/listinfo/haskell
Re: Functional dependencies and Constructor Classes
Martin Sulzmann [EMAIL PROTECTED] writes:
Hi,
I was wondering whether other people made similiar observations.
Functional dependencies seem to be expressiveness enough to encode
some of the kinding rules required for Constructor Classes.
read this page:
http://cvs.haskell.org/Hugs/pages/hugsman/exts.html
I think that the designer of constructor class and functionnal depedencies is the same
person si it makes sense that one generalise the other.
nevertheless i found constructor class more elegant for many problems.
Your solution is less elegant that the one using constructor classes.
I found too that type error messages of class using functionnal depedencies
are not easy to read. There is often ambiguity in code that are not easy to solver.
this problem does not appear with constructor classes.
Take a look at the Haskell code below
(runs under hugs -98 or ghci -fglasgow-exts-fallow-undecidable-instances)
Martin
-- An alternative to constructor classes
module Fmap where
{- Instead of
class Functor f where fmap :: (a-b)-(f a-f b)
use
-}
class Fmap a b fa fb | a fb - b fa,
b fa - a fb,
fa fb - a b
where fmap2 :: (a-b)-(fa - fb)
{- We require:
(1) fmap2 transforms a function into another function,
i.e. fmap2's type should always be of shape (a-b)-(fa-fb)
(2) b, fa uniquely determine a and fb
(3) a, fb b and fa
(4) fa, fb a and b
Note that (1) is enforced by the class definition. (2)-(4) are enforced by FDs.
My guess/conjecture is that the above axiomatization of functors is equivalent to the
one found in Haskell98.
-}
-- some Examples
{- The following is a variation of an example taken from Mark Jones original paper
A System of Constructor Classes: Overloading and Implicit Higher-Order
Polymorphism.
He used this example to motivate the introduction of constructor classes. The example
is type correct using the alternative formulation of functors.
-}
cmap :: (Fmap a b fb1 fb, Fmap a1 b1 fa fb1) =
(a1 - b1) - (a - b) - fa - fb
cmap f g = (fmap2 g) . (fmap2 f)
-- identity functor
instance Fmap a a a a where fmap2 h = h
-- functor composition
-- Instance is not allowed, cause leads to undecidable type inference
{-
instance (Fmap a b c d, Fmap e f a b) = Fmap e f c d
where fmap2 h = fmap2 (fmap2 h)
-}
comp :: (Fmap fa1 fb1 fa fb, Fmap a b fa1 fb1) =
(a - b) - fa - fb
comp h = fmap2 (fmap2 h)
___
Haskell mailing list
[EMAIL PROTECTED]
http://www.haskell.org/mailman/listinfo/haskell
--
Yoann Padioleau, INSA de Rennes, France,
Opinions expressed here are only mine. Je n'écris qu'à titre personnel.
** Get Free. Be Smart. Simply use Linux and Free Software. **
___
Haskell mailing list
[EMAIL PROTECTED]
http://www.haskell.org/mailman/listinfo/haskell
Re: Functional dependencies and Constructor Classes
Yoann Padioleau writes: nevertheless i found constructor class more elegant for many problems. Your solution is less elegant that the one using constructor classes. Yes, the current presentation of constructor classes might be easier to comprehend. I found too that type error messages of class using functionnal depedencies are not easy to read. There is often ambiguity in code that are not easy to solver. this problem does not appear with constructor classes. Well, that's the point of my encoding of functors using FD's. No ambiguities will arise! The issue I want to raise is whether constructor classes are redundant in the presence of FDs (yes, yes, we still might want to stick to the constructor class representation, but that's a different issue). Martin ___ Haskell mailing list [EMAIL PROTECTED] http://www.haskell.org/mailman/listinfo/haskell
RE: Functional dependencies and Constructor Classes
Hi Martin, | The issue I want to raise is whether constructor classes are | redundant in the presence of FDs No, they are not comparable. Let fds = functional dependencies ccs = constructor classes Example of something you can do with ccs but not fds: data Fix f = In (f (Fix f)) Example of something you can do with fds but not ccs: class Collects e ce where ... -- see fds paper for details instance Eq e = Collects e [e] where ... instance Eq e = Collects e (e - Bool) where ... Your fds version of the Functor class is also incomparable with the ccs version; the former will allow an expression like (map id 'a') to be type checked, the latter will not, treating it instead as a type error. In this specific case you may regard the extra flexibility provided by fds as a win for expressiveness. On another occasion, however, you may be disappointed to discover that you have delayed the detection of a type error from the point where it was introduced. There's a lot more that could be said about this, but I don't have time to go into detail now. Hopefully, I have at least answered your basic question. The approach you've suggested using fds reminds me most directly of the work on Parametric Type Classes (PTC) by Chen, Hudak and Odersky. In my paper on Functional dependencies, I made the following comment regarding that work: Thus, PTC provides exactly the tools that we need to define and work with a library of collection classes. In our opinion, the original work on PTC has not received the attention that it deserves. In part, this may be because it was seen, incorrectly, as an alternative to constructor classes and not, more accurately, as an orthogonal extension. I believe the same is true in this case. Ccs and fds address different problems. They are complementary tools, each with their own strengths and weaknesses. All the best, Mark Refs: for those who want to follow along: Type Classes with Functional Dependencies http://www.cse.ogi.edu/~mpj/pubs/fundeps.html Constructor Classes http://www.cse.ogi.edu/~mpj/pubs/fpca93.html (But read the JFP version instead if you can; it's much better ...) ___ Haskell mailing list [EMAIL PROTECTED] http://www.haskell.org/mailman/listinfo/haskell
RE: functional dependencies
I'm just catching up with some old mail here. Iavor writes: | class C a b | a - b | class C a b = D a | | vs. | | class C a b | a - b | class C a b = D a b | | Hugs accepts both of those, while GHC insists on the second. | The first example is a little shorter and one might argue that if we | know a we also know b, because of the functional depency, | so it is not really a parameter. | | On the other hand, i would expect writing b in the type | signatures of any of the methods to refer to the particular b | determined by the a, rather than it becomeing universally | quantified, and perhaps this is more explicit in the second form. Dead right! Imagine there was a method in class D: class C a b = D a where op :: a - b The type of 'op' is op :: D a = a - b You can't really expect that the 'b' here is determined by 'a'! Still, I suppose that if the methods in class D mention only 'a', then it is strange to require D to be parameterised over 'b'. Thus, this seems more reasonable: class C a b = D a where op :: a - a Even this seems odd, because we would get the deduction D a |- C a b (i.e. from a (D a) dictionary you can get a (C a b) dictionary) and that's only true for a particular 'b'. My brain is too small to be sure what I'm talking about here, but I'm strongly inclined to be conservative here, which GHC is. Simon ___ Haskell mailing list [EMAIL PROTECTED] http://www.haskell.org/mailman/listinfo/haskell
RE: functional dependencies - bug?
Christian This is clearly a bug in 5.03. However, it works fine in the (about to be released) 5.04. My plan, therefore, is to add it to our regression test suite and delcare victory. If I was being totally thorough I'd find out what went wrong in 5.03, in case it's still wrong in 5.04, but I'm not going to be totally thorough! Please yell if any similar mysterious things happen. I appreciate the report. Simon | -Original Message- | From: Christian Maeder [mailto:[EMAIL PROTECTED]] | Sent: 28 June 2002 18:09 | To: [EMAIL PROTECTED] | Subject: functional dependencies - bug? | | | Hi, | | does anybody have experiences with Type Classes with | Functional Dependencies (LNCS 1782, ESOP 2000, March 200, by | Mark P. Jones)? | | I've tried the example in the above paper: | | class Collects e ce | ce - e where | empty :: ce | insert :: e - ce - ce | member :: e - ce - Bool | | This works correctly for: | | instance Eq a = Collects a [a] where | instance Collects Char Int where | | and complains correctly for: | | instance Collects Char Int where | instance Collects Bool Int where | | with Functional dependencies conflict between instance declarations | | Now to my problem with a context in the class declaration: | | class Eq ce = Collects e ce | ce - e where | empty :: ce | ... | | This works as above, but correctly complains for: | | data Stupid = Stupid -- without equality | instance Collects Bool Stupid where | | with No instance for (Eq Stupid). | | However, if I supply an (admittingly stupid) default | definition for empty within the class declaration: | | class Eq ce = Collects e ce | ce - e where | empty :: ce | empty = error(empty) | ... | | I no longer get the above No instance for (Eq | Stupid)-Message, and I guess that is a bug (or a feature | that I don't understand). | | When I change the context to Eq e everything is fine again: | | instance Collects Stupid Int where | | complains as above. | | I don't know when (even meaningful) default definitions cause | that context conditions are not checked. In fact I noticed | this error only after I've removed a default definition just | to find out that my instance declaration were wrong that | seemed to be correct before (but instances for contexts were missing). | | Are there any other (known) pitfalls with functional dependencies? | | Regards Christian ___ | Glasgow-haskell-users mailing list | [EMAIL PROTECTED] | http://www.haskell.org/mailman/listinfo/glasgow-| haskell-users | ___ Glasgow-haskell-users mailing list [EMAIL PROTECTED] http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
Re: Functional dependencies
Marcin 'Qrczak' Kowalczyk wrote: Thank you for ghc-4.06! The following code is accepted by Hugs, but ghc complains about type variable r being not in scope. Adding "forall m r." causes the error "each forall'd type variable mentioned by the constraint must appear after the =", where Hugs still accepts it. If I understand functional dependencies, they should be legal. With a concrete monad fundeps work. class Reference r m | m - r where new :: a - m (r a) put :: r a - a - m () get :: r a - m a test:: (Monad m, Reference r m) = m Int test = do x - new 42 get x Functional dependencies fall under the category of "Not-quite-ready-yet, but in there nontheless". But thanks for the report. Functional dependencies and implicit params won't be fully supported 'till a later release (hopefully the next one). --Jeff
RE: Functional Dependencies
Hi Fermin, | Should redundant dependencies trigger an error or a warning? I'd | say that if I'm writing some haskell code, I wouldn't mind if a | redundancy is flagged as an error; most likely, it'd take a short | time to fix. However, if someone is generating haskell automatically | (maybe with Derive, PolyP, a GUI designer, ...), the easiest thing | to do is to generate all the dependencies that will make the types | correct, without trying to avoid redundancies. In this case, | I think a warning is better. Generating a warning instead of an error might indeed be preferable. But I disagree with your motivation. Except in cases where a language is specifically designed to be used as a target such programs, I believe that implementations should be optimized for the benefit of their human users. For the comparatively rare cases where someone is writing a program that generates Haskell class definitions, including dependencies, it surely isn't too much to expect them to add a line or two to filter out any that are redundant? After all, they are probably having to work much harder just to pretty print the rest of the text. A better solution still would be to have a standardized library called HaskellSyntax, which all of the code generating tools that you describe (and more!) could use. The module would export a set of datatypes for describing the abstract syntax of Haskell programs and an associated set of pretty printers. (Or perhaps the printer functions by themselves would be enough?) The pretty printers would take care of all those minor little issues like deciding when parentheses were needed, when an operator should be written with applicative or infix syntax, breaking long strings across line boundaries, etc. It could also take care of filtering out redundant dependencies, for example, if this was considered useful. I think this would be a neat library to have around, especially if the authors of tools like Derive, PolyP, H/Direct, Happy, or anything else that generates Haskell code could be persuaded to use it. I hope somebody will take up the challenge! All the best, Mark
Re: Functional Dependencies
Mark P Jones wrote: | | Neat. And it solves a problem I was kludging around with explicit, | | existentially quantified dictionaries. | | Great! Can I look forward to hearing more about that some time? OK, it's to do with arrows: class Arrow a where arr :: (b - c) - a b c () :: a b c - a c d - a b d first :: a b c - a (b,d) (c,d) Given an arrow a, I want to form a new arrow newtype Instance f a b c = Inst (a (f b) (f c)) Defining arr and is easy (provided f is a functor and a an arrow), but to define first, we need an isomorphism between f(b,c) and (f b,g b) for some functor g. Some examples: f g (,) s Id state transformers Stream Stream synchronous circuits (-) s (-) s a version of Dick Kieburtz's co-state comonad With functional dependencies, I can presumably write class (Functor f, Functor g) = Zippable f g | f - g where unzipper :: f(b,c) - (f b, g c) zipper :: (f b, g c) - f(b,c) instance Zippable ((-) s) ((-) s) where unzipper f = (fst . f, snd . f) zipper (f,g) x = (f x, g x) instance (Zippable f g, Arrow a) = Arrow (Instance f a) where arr f = Inst (arr (fmap f)) Inst f Inst g = Inst (f g) first (Inst f) = Inst (arr unzipper first f arr zipper) The type constructor g only features inside the last composition; none of the top-level things have types that mention g, so doing this without dependencies isn't easy. The kludge I used was an explicit dictionary data ZipD f = forall g. ZipD (forall b,c. f(b,c) - (f b, g c)) (forall b,c. (f b, g c) - f(b,c)) and a class class Functor f = Zippable f where zipD :: ZipD f Defining an instance looked like this: instance Zippable ((-) s) where zipD = ZipD unzipper zipper where unzipper f = (fst . f, snd . f) zipper (f,g) x = (f x, g x) Then I could define the arrow: instance (Zippable f, Arrow a) = Arrow (Instance f a) where arr f = Inst (arr (fmap f)) Inst f Inst g = Inst (f g) first (Inst f) = Inst (arr unzipper first f arr zipper) where ZipD unzipper zipper = zipD This kludge only handles situations where a subset of the arguments are dependent on the rest.
Re: Functional Dependencies
Mark P Jones wrote: A couple of months ago, I developed and implemented an extension to Hugs that has the potential to make multiple parameter type classes more useful. The key idea is to allow class declarations to be annoted with `functional dependencies'---an idea that has previously received rather more attention in the theory of relational databases. Neat. And it solves a problem I was kludging around with explicit, existentially quantified dictionaries. On a superficial note, how about class C a b c | (a,b) = c where ... for class C a b c | a b - c where ... etc? Also, you say a dependency with zero variables on the right side is syntactically correct, but later you say it will be reported as an error because it says nothing. Why bother? -- Ross Paterson
RE: Functional Dependencies
| Also, you say a dependency with zero variables on the right side is
| syntactically correct, but later you say it will be reported as an
| error because it says nothing. Why bother?
Point taken. In fact that same database text I mentioned above
prohibits functional dependencies in which either side is empty.
But it turns out that the two extremes ("a -" and "- a") are
rather interesting so I didn't want to exclude either as being
syntactically well-formed. Rejecting the former at a later stage
was a design decision, intended only to catch errors, and isn't
an essential part of the design.
All the best,
Mark
Should redundant dependencies trigger an error or a warning? I'd say that if
I'm writing some haskell code, I wouldn't mind if a redundancy is flagged as
an error; most likely, it'd take a short time to fix. However, if someone is
generating haskell automatically (maybe with Derive, PolyP, a GUI designer,
...), the easiest thing to do is to generate all the dependencies that will
make the types correct, without trying to avoid redundancies. In this case,
I think a warning is better.
Just my 2 cents.
Fermin
Re: Functional Dependencies
Hi Mark,
at the end of section 2 of http://www.cse.ogi.edu/~mpj/fds.html you
might want to mention that there is a "standard" work-around whenever a
type constructor is needed but not available: Introduce a newtype.
import Bits
class Collects e c where
empty :: c e
insert :: e - c e - c e
member :: e - c e - Bool
instance Eq e = Collects e [] where
empty = []
insert = (:)
member = elem
Apply the work-around for characteristic functions.
newtype CharacteristicFunction e = CF {unCF :: e - Bool}
instance Eq e = Collects e CharacteristicFunction where
empty = CF (\y - False)
insert x c = CF (\y - x == y || unCF c x)
member x c = unCF c x
Apply the work-around for bit sets. The dummy type variable "a" is
needed to make "BitSet b" a type constructor. (I've also generalized
your example from Char to Enum.)
newtype Bits b = BitSet b a = BS {unBS :: b}
instance (Enum e, Bits b) = Collects e (BitSet b) where
empty = BS (bit 0)
insert x c = BS (setBit (unBS c) (fromEnum x))
member x c = testBit (unBS c) (fromEnum x)
For the hash-table example I am pretty sure that the work-around works
as well, even though I could not figure out your intended
implementation.
Of course this is just a work-around and does not make functional
dependencies superfluous.
Regards,
Heribert.
RE: Functional Dependencies
Hi Heribert, Thanks for your feedback! | at the end of section 2 of http://www.cse.ogi.edu/~mpj/fds.html you | might want to mention that there is a "standard" work-around whenever a | type constructor is needed but not available: Introduce a newtype. Yes, an in fact this idea is mentioned at the end of the constructor classes paper!). But it doesn't always work, and, even when it does, you have to deal with the extra newtype constructors in both types and terms. The BitSet example shows when it doesn't work ... your reworking of that example depended on generalizing the collection type to add an extra parameter. But suppose that you didn't want to, or couldn't, make that generalization. For example, this might occur (and indeed, has occurred in some of our experiments at OGI) in programs that package up somebody else's code to be used via a class. And if you can't generalize, then you're stuck. | For the hash-table example I am pretty sure that the work-around works | as well, even though I could not figure out your intended | implementation. For the hash table example, one possible newtype encoding might be as follows: newtype HTable bucket a = Array Int (bucket a) instance (Hashable a, Collects a b) = Collects a (HTable b a) where ... But this has some problems too ... suppose (somewhat bizarrely in this case perhaps) that you wanted to use a composition of two collection types to build the bucket type. The type of the corresponding collection would be: Array Int (outer (inner a)). This would work just fine with the functional dependencies version, but for the constructor classes version you'd have to introduce yet another newtype and instance: newtype Compose f g x = Comp (f (g x)) instance (Collects a g, Collects (g a) f) = Collects a (Comp f g) where ... And so on ... | Of course this is just a work-around and does not make functional | dependencies superfluous. That's true. There are plenty of things you can do with dependencies that you can't do with constructor classes, and vice versa. I picked the Collects example because I thought it would be something that would be reasonably familiar, but perhaps it has the danger of giving people the impression that functional dependencies are an alternative to constructor classes. That's unfortunate because they're really pretty orthogonal. All the best, Mark
