Functional Dependencies

[Mark P Jones]

[Simon mentioned my work on `functional dependencies' in one of his
messages a couple of days ago, so I thought I'd better post an
explanation!]

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.
For example, we could use the following declaration as the starting
point for a simple `collection' class library:

   class Collects e ce | ce -> e where
  empty  :: ce
  insert :: e -> ce -> ce
  member :: e -> ce -> Bool

The new part here is the clause "| ce -> e", which tells us that the
"ce" parameter (the type of the collection) uniquely determines the
"e" parameter (the type of the elements).  Dependencies like this
can be used to avoid ambiguity problems; to obtain more accurate, and
less cluttered inferred types; and to allow more general sets of
instances than constructor classes.  If this has got your interest,
you can find more information at http://www.cse.ogi.edu/~mpj/fds.html.

Support for this extension is included in the imminent September 1999
release of Hugs 98.  In the meantime, Jeff Lewis, a colleague here at
OGI, has been putting together an implementation for GHC.  I've also
written a longer paper that gives more technical details, and explains
how this idea fits in with other work, but there are a few things I
want to do to that before it is ready for distribution, probably after
I get back from the Haskell Workshop.

I hope folks will find this useful.  A month or two back, somebody on
this list said that we had no `peer review' process ... people
just do something, then say "here it is, use it".  Well I've done
something ... here it is ... I hope that some of you will use it ...
and I do very much appreciate your feedback.  The peer review
starts today!

All the best,
Mark

functional dependencies

[Iavor S. Diatchki]

hello,

there seems to be a difference between the way superclasses are handled in 
GHC and Hugs, and it would be nice if one of the choices was selected
(i am not sure what other implementations do).  here is what i mean:

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.  

bye
iavor
___
Haskell mailing list
[EMAIL PROTECTED]
http://www.haskell.org/mailman/listinfo/haskell

functional dependencies

[Johannes Waldmann]

Can I write dependencies like this:
 
> class C x y z | x -> (y, z) 
> class D x y z | (x, y) -> z

in hugs? in ghc? The ghc doc refers to  
Mark Jones: "Type Classes with Functional Dependencies",
http://www.cse.ogi.edu/~mpj/pubs/fundeps.html
where this seems to be allowed (section 4, page 9)

Especially, I would need class D above. 
-- 
-- Johannes Waldmann  http://www.informatik.uni-leipzig.de/~joe/ --
-- [EMAIL PROTECTED] -- phone/fax (+49) 341 9732 204/252 --
___
Haskell mailing list
[EMAIL PROTECTED]
http://www.haskell.org/mailman/listinfo/haskell

Re: Functional Dependencies

[Heribert Schuetz]

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

[Mark P Jones]

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

RE: Functional Dependencies

[Mark P Jones]

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

[Ross Paterson]

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

[Fermin Reig Galilea]

> 
> | 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

[Mark P Jones]

| 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?

| 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?

The current syntax was chosen because it was the same as in one of
the database texts that I looked at.  It also doesn't require any
new symbols in the lexical syntax.   But I don't have any strong
views about this, and it's all open for discussion.  What you've
suggested here seems like another reasonable alternative, that also
satisfies the no new symbols property.

| 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

Re: Functional Dependencies

[Ross Paterson]

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

[Simon Peyton-Jones]

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

[Ashley Yakeley]

At 2002-07-23 09:06, Simon Peyton-Jones wrote:

>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'!

Agreed. If you were going to allow "D a", they would have to be 
considered different "b"s.

>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'. 

Well that's OK. From a (D a) dictionary, you get a (C a b) dictionary, 
where you're given "a", and you can find "b" from the fundep.

-- 
Ashley Yakeley, Seattle WA

___
Haskell mailing list
[EMAIL PROTECTED]
http://www.haskell.org/mailman/listinfo/haskell

Problem with functional dependencies

[Marcin 'Qrczak' Kowalczyk]

The following module is rejected by both
ghc -fglasgow-exts -fallow-undecidable-instances
and
hugs -98


class HasFoo a foo | a -> foo where
foo :: a -> foo

data A = A Int
data B = B A

instance HasFoo A Int where
foo (A x) = x

instance HasFoo A foo => HasFoo B foo where
foo (B a) = foo a


The error messsage says that the type inferred for foo in B's instance
is not general enough: the rhs has type "HasFoo B Int => B -> Int", but
"HasFoo B foo => B -> foo" was expected.

Should it really be wrong? I don't know the details of type inference
with fundeps, but intuitively it should work, yielding an instance
HasFoo B Int. Could it be made legal please?

With the fundep removed, it works.

I need it for a preprocessor which generates instances like that for B
without knowing the type to put as the second class argument. Fundeps
aren't essential, but...

-- 
 __("<  Marcin Kowalczyk * [EMAIL PROTECTED] http://qrczak.ids.net.pl/
 \__/
  ^^  SYGNATURA ZASTÊPCZA
QRCZAK


___
Haskell mailing list
[EMAIL PROTECTED]
http://www.haskell.org/mailman/listinfo/haskell

inference with functional dependencies

[Avi Pfeffer]

Inferring equality between types when there are functional dependencies
seems to be less powerful than I expected.  Here's a simple example:

class Eq b => C a b | a -> b

data T a = forall b . C a b => T b
data U a = forall b . C a b => U b

compare :: T a -> U a -> Bool
compare (T x) (U y) = x == y

I expected the compiler (GHC) would be able to deduce that the b type in
the representation of T a and U a must be the same, since both stand in a
C a b relationship, and a functionally determines b in that
relationship.  Instead I get the message:

Inferred type is less polymorphic than expected
Quantified type variable `b1' is unified with `b'
When checking a pattern that binds
x :: b
y :: b1
In an equation for function `Test.compare':
Test.compare (T x) (U y) = x == y

Is this expected behavior?  Is there a way for me to provide the necessary
hints so that code like this could be accepted?

Thanks,
  Avi Pfeffer
--
Avi Pfeffer[EMAIL PROTECTED] www.eecs.harvard.edu/~avi
Maxwell Dworkin 251
Division of Engineering and Applied Sciences  Tel: (617) 496-1876
Harvard UniversityFax: (617) 496-1066



___
Haskell mailing list
[EMAIL PROTECTED]
http://www.haskell.org/mailman/listinfo/haskell

Syntax of functional dependencies

[Till Mossakowski]

I errorneously specified categories as

class (Eq object, Eq morphism) => 
  Category id object morphism | id ->, id -> morphism
  where  o :: id -> morphism -> morphism -> Maybe morphism
 dom, cod :: id -> morphism -> object

it should have been

class (Eq object, Eq morphism) => 
  Category id object morphism | id -> object, id -> morphism
  ... ^^

- but ghci 5.02.2 does not complain. Why?

Till Mossakowski

-- 
Till MossakowskiPhone +49-421-218-4683
Dept. of Computer Science   Fax +49-421-218-3054
University of Bremen[EMAIL PROTECTED]   
P.O.Box 330440, D-28334 Bremen  http://www.tzi.de/~till
___
Haskell mailing list
[EMAIL PROTECTED]
http://www.haskell.org/mailman/listinfo/haskell

Functional dependencies and improvement

[Martin Sulzmann]

Hi,

yet again FD's! In my previous example I employed FD's to improve
constraints. However, there are cases where FD's seem to be overly
restrictive. Take a look at the Haskell code below. Have others
made similar experiences?

Martin



-- FDs are sometimes overly restrictive

module Insert where

class Insert a b | b -> a where insert :: a->b->b

class Leq a where leq :: a->a->Bool

instance Leq a => Insert a [a]
-- we're not so interested in the values for the purpose of this example


-- hugs or ghc will complain about the following instance
instance Insert Int [Float]
-- though this makes sense! Elements of value Int should allowed to be stored as Floats


{- Reason: Improvement in case of FDs seems overly restrictive

Consider Mark Jones paper "Type Classes with Functional Dependencies", page 12, 
Section 6.2.

In case of the above type class we require that
for each constraint Insert t1 t2 and declaration

 instance C => Insert t1' t2' where

if phi(t2) = t2' then phi(t1) = t1' for some substitution phi.
However, we have that phi([a]) = [Float] and phi(a) \not= Int where
phi=[a |-> Float]. The problem is that the improvement strategy
does not take into account the context in the instance declaration.

Solution:
We should only improve 'Insert a [b]' to 'Insert b [b]' where phi=[a |-> b]
in case we additionally find 'Leq b'. Though, this cannot be specified
with FD's.

-}

___
Haskell mailing list
[EMAIL PROTECTED]
http://www.haskell.org/mailman/listinfo/haskell

RE: Problem with functional dependencies

[Simon Peyton-Jones]

I think you can simplify the example.  Given

class HasFoo a b | a -> b where
  foo :: a -> b

instance HasFoo Int Bool where ...

Is this legal?

f :: HasFoo Int b => Int -> b
f x = foo x

You might think so, since 
HasFoo Int b => Int -> b
is a substitution instance of
HasFoo a b => a -> b

but if we infer the type (HasFoo Int b => Int -> b)
for f's RHS, we can then "improve" it using the instance
decl to (HasFoo Int Bool => Int -> Bool), and now the signature
isn't a substitution insance of the type of the RHS.  Indeed,
this is just what will happen if you try with GHC, because
GHC takes advantage of type signatures when typechecking a 
function defn, rather than first typechecking the defn and only
then comparing with the signature.

I don't know what the answers are here, but there's more to this
functional dependency stuff than meets the eye.  Even whether
one type is more general than another has changed!

Simon

| -Original Message-
| From: [EMAIL PROTECTED] [mailto:[EMAIL PROTECTED]]
| Sent: 17 December 2000 19:30
| To: [EMAIL PROTECTED]
| Subject: Problem with functional dependencies
| 
| 
| The following module is rejected by both
| ghc -fglasgow-exts -fallow-undecidable-instances
| and
| hugs -98
| 
| --
| --
| class HasFoo a foo | a -> foo where
| foo :: a -> foo
| 
| data A = A Int
| data B = B A
| 
| instance HasFoo A Int where
| foo (A x) = x
| 
| instance HasFoo A foo => HasFoo B foo where
| foo (B a) = foo a
| --
| --
| 
| The error messsage says that the type inferred for foo in B's instance
| is not general enough: the rhs has type "HasFoo B Int => B -> 
| Int", but
| "HasFoo B foo => B -> foo" was expected.

___
Haskell mailing list
[EMAIL PROTECTED]
http://www.haskell.org/mailman/listinfo/haskell

Re: Problem with functional dependencies

[Jeffrey R. Lewis]

Simon Peyton-Jones wrote:

> I think you can simplify the example.  Given
>
> class HasFoo a b | a -> b where
>   foo :: a -> b
>
> instance HasFoo Int Bool where ...
>
> Is this legal?
>
> f :: HasFoo Int b => Int -> b
> f x = foo x
>
> You might think so, since
> HasFoo Int b => Int -> b
> is a substitution instance of
> HasFoo a b => a -> b

This is the step where the reasoning goes wrong.  The functional dependency tells you 
that `b' isn't really a free variable, since it is dependent on `a'.  If you 
substitute for `a', you can't expect `b' to remain unconstrained.

Hugs complains that the inferred type for `f' is not general enough.  It's right to 
complain, but the real problem is that the signature is too general.  Asimilar 
situation arises if you try to declare an instance `HasFoo Int b', but in this case, 
hugs complains that the instance is more general than the dependency allows.  A useful 
thing to do would be to check for this sort of thing in signatures as well, so that 
the more appropriate error message can be given.

--Jeff


___
Haskell mailing list
[EMAIL PROTECTED]
http://www.haskell.org/mailman/listinfo/haskell

Re: Problem with functional dependencies

[Marcin 'Qrczak' Kowalczyk]

Thu, 21 Dec 2000 00:59:29 -0800, Jeffrey R. Lewis <[EMAIL PROTECTED]> pisze:

> > class HasFoo a b | a -> b where

> > f :: HasFoo Int b => Int -> b
> > f x = foo x

> This is the step where the reasoning goes wrong.  The functional
> dependency tells you that `b' isn't really a free variable, since
> it is dependent on `a'.  If you substitute for `a', you can't expect
> `b' to remain unconstrained.

It's not unconstrained: the constraint is "HasFoo Int b", as written.
IMHO it should not matter that the constraint fully determines b.

> Asimilar situation arises if you try to declare an instance `HasFoo
> Int b', but in this case, hugs complains that the instance is more
> general than the dependency allows.

ghc does not complain. How would I express "the instance can be chosen
basing on 'a' alone, and the instance found will tell what constraints
are on 'b'"?

Aren't fundeps a too general mechanism which is not able to express
simpler statements? :-(

-- 
 __("<  Marcin Kowalczyk * [EMAIL PROTECTED] http://qrczak.ids.net.pl/
 \__/
  ^^  SYGNATURA ZASTÊPCZA
QRCZAK


___
Haskell mailing list
[EMAIL PROTECTED]
http://www.haskell.org/mailman/listinfo/haskell

Re: Problem with functional dependencies

[Lennart Augustsson]

Simon Peyton-Jones wrote:

> I think you can simplify the example.  Given
>
> class HasFoo a b | a -> b where
>   foo :: a -> b
>
> instance HasFoo Int Bool where ...
>
> Is this legal?
>
> f :: HasFoo Int b => Int -> b
> f x = foo x
>
> You might think so, since
> HasFoo Int b => Int -> b
> is a substitution instance of
> HasFoo a b => a -> b
>
> but if we infer the type (HasFoo Int b => Int -> b)
> for f's RHS, we can then "improve" it using the instance
> decl to (HasFoo Int Bool => Int -> Bool), and now the signature
> isn't a substitution insance of the type of the RHS.

I definitely want it to be legal.  I have examples where this is immensly useful.


--

-- Lennart




___
Haskell mailing list
[EMAIL PROTECTED]
http://www.haskell.org/mailman/listinfo/haskell

RE: Problem with functional dependencies

[Mark P Jones]

| I think you can simplify the example.  Given
| 
|   class HasFoo a b | a -> b where
| foo :: a -> b
|   instance HasFoo Int Bool where ...
| 
| Is this legal?
|   f :: HasFoo Int b => Int -> b
|   f x = foo x

The theoretical foundation for functional dependencies goes back to
the work I did on "Simplifying and Improving Qualified Types".
(Interested parties can find a 1994 report on this on my web pages;
email me if you need a pointer.)

According to that theory, the type above is a "principal satisfiable
type" for f, as is the more accurate Int -> Bool: under the
satisfiability ordering described in the report, these two types
are (satisfiably) equivalent.  There is, therefore, no technical
reason why the function f could not be treated as having the
polymorphic type shown above.

On the other hand, from a practical perspective, one can argue that
the polymorphic type is misleading, obfuscating, and cumbersome:
Misleading because f doesn't really have a polymorphic type as the
declaration pretends; Obfuscating because it forces a reader to
study instance declarations that are not included in the type;
and Cumbersome because it includes an unnecessary (HasFoo Int b)
constraint that could be eliminated to produce a shorter, simpler
type.

So it comes down to a language design *decision* for which functional
dependencies, by themselves, do not force a particular choice.

- The current Hugs implementation does not allow the polymorphic
  type; the intention in that implementation was to infer more
  accurate, less complex types.  The idea here is to make programs
  easier for programmers to read, write, and understand.

- Marcin indicates that he would prefer the more relaxed approach
  that allows polymorphic types; he is writing a preprocessor that
  generates type signatures, and his task is easier if he doesn't
  have to worry about the "improvement" of class constraints.
  The idea here is to make programs easier for generators to read,
  write and manipulate.

Clearly, some compromise is needed because neither approach is right
for all purposes.  If we look to other aspects of the language for
inspiration, then the best way to deal with this is (probably):
  (i) to infer simpler types whenever possible, but
 (ii) to allow more polymorphic types when they are requested by
  means of an explicit type signature.
(Incidentally, in the interests of consistency, such a system should
also programmers to use types like  Num Int => Int -> Bool.)

All the best,
Mark


___
Haskell mailing list
[EMAIL PROTECTED]
http://www.haskell.org/mailman/listinfo/haskell

Re: Problem with functional dependencies

[Fergus Henderson]

On 03-Jan-2001, Mark P Jones <[EMAIL PROTECTED]> wrote:
> ... the best way to deal with this is (probably):
>   (i) to infer simpler types whenever possible, but
>  (ii) to allow more polymorphic types when they are requested by
>   means of an explicit type signature.

I agree.

> (Incidentally, in the interests of consistency, such a system should
> also programmers to use types like  Num Int => Int -> Bool.)

Mercury uses the approach you've suggested above for constraints like
these.  That is, you can declare types like that, and the Mercury
type checker will accept them, but it won't try to infer such types.

This feature could be a bit more useful in Mercury than in Haskell,
since in Mercury instance declarations can be private to a particular
module.

(Unfortunately, though, the Mercury runtime system's RTTI
representation of instances is not able to handle such constraints, so
for such examples, the current implementation of the compiler reports
"sorry, not implemented: constraints may only constrain type variables".)

-- 
Fergus Henderson <[EMAIL PROTECTED]>  |  "I have always known that the pursuit
|  of excellence is a lethal habit"
WWW:   | -- the last words of T. S. Garp.

___
Haskell mailing list
[EMAIL PROTECTED]
http://www.haskell.org/mailman/listinfo/haskell

Re: Problem with functional dependencies

[Marcin 'Qrczak' Kowalczyk]

I don't fully understand fundeps. Would the following transform
legal programs (without overlapping instances) into legal programs?
I hope yes.

Let's imagine a class with a set of instances and uses, without
fundeps.

- Add some additional type variables to the class header.
- Add a fundep: all old type variables -> all new type variables.
- For each instance, in places corresponding to new type variables
  write arbitrary types.
- For each constraint based on this class, in places corresponding
  to new type variables write unique type variables.

In particular, should the following be legal:

class C a b c | a -> b c
instance C [a] b b
f:: C [a] b c => a
f = undefined

ghc panics and Hugs rejects it.

-- 
 __("<  Marcin Kowalczyk * [EMAIL PROTECTED] http://qrczak.ids.net.pl/
 \__/
  ^^  SYGNATURA ZASTÊPCZA
QRCZAK


___
Haskell mailing list
[EMAIL PROTECTED]
http://www.haskell.org/mailman/listinfo/haskell

RE: Problem with functional dependencies

[Mark P Jones]

Hi Marcin,

| In particular, should the following be legal:
| 
| class C a b c | a -> b c
| instance C [a] b b
| f:: C [a] b c => a
| f = undefined
| 
| ghc panics and Hugs rejects it.

No, it is not legal.  Even if you delete the definition of f, the code
is still not legal because the class and the instance declaration are
inconsistent.

The class declaration says that you want to define a three place relation
on types called C.  We can think of the entries in this relation as rows
in a table with columns headed a, b, and c:

   a  |  b  |  c
 C = -+-+--
  | |

Before we take a look at any instance declarations, this table is empty
(i.e., there are no rows).  But the functional dependency a -> b c that
you have specified establishes a constraint that any data that gets added
to the table by subsequent instance declarations must satisfy.  It says
that, if two rows have the same type in the a column, then they must also
have the same types in the b and c columns; "the values of b and c are
uniquely determined by the value of a."

So here are two plausible instance declarations that you could use:

  instance C Int Int Char
  instance C (Maybe t) t Int

Notice that the second declaration here is really an instance scheme;
the presence of a variable "t" means that it introduces a whole family
of instances, one for each possible instantiation of the variable "t".

With these two instance declarations in hand, our table looks something
like the following:

 a | b |  c
 C = --+---+--
Int|   Int | Char
Maybe Int  |   Int | Int
Maybe Bool |   Bool| Int
Maybe Char |   Char| Int
Maybe [Int]|   [Int]   | Int
 Maybe (Maybe Int) | Maybe Int | Int
...|...| ...

Conceptually, of course, there are now infinitely many rows in the table,
so what you see here is just a small part of the relation.  But notice that
the data in the table is entirely consistent with the functional dependency
a -> b c because no two rows have the same type in the a column.

Now consider the instance declaration that you have given:

  instance C [t] s s

Again, this is an instance scheme, generating one row in the table
for each possible instantiation of variables "t" and "s".  (To avoid
confusion with the names of the columns in C, I've chosen different
variable names from the ones you've used.)  For example, based on
this instance declaration, we would expect to continue adding rows
to the table along the following lines:

  a  |   b   |   c
 C = +---+---
[Int]|  Int  |  Int   t=Int, s=Int
[Int]|  Bool |  Bool  t=Int, s=Bool
[Bool]   |  Int  |  Int   t=Bool, s=Int
 ... |  ...  |  ...

I hope now that the problem is becoming clear: this instance declaration
is not consistent with the dependency; in the first two lines above, for
example, we see two rows that violate the specification because they have
the same value of "a", but different values for "b" and "c".

In summary, the class declaration and its associated dependency are not
consistent with the instance declaration.  If you really wanted the rows
described by the instance declaration to be part of the relation C, then
the dependency you have written is not valid.  If you really did want the
restriction captured by the dependency, then the instance declaration is
not valid.  Hugs can't tell which of these is the real source of the
problem, but it does report, correctly, that there is an inconsistency.

A little more generally, given the class declaration and the dependency
that you've specified, Hugs will not allow any instance declaration for
something of the form  C t1 t2 t3  if there are variables in t2 or t3
that do not appear in t1.  If this restriction were not enforced, then
it would again be possible for there to be multiple rows with the same
"a" value, but different "b" and "c" entries.

I noticed the same problem in one of the earlier examples that you sent
to the list:

| class Foo a b | a
| instance Foo Int [a]
| -- This is rejected by Hugs (with fundep a->b) but I would definitely
| -- accept it.

I hope that it is now clear why Hugs rejects this definition.

| I don't fully understand fundeps.

The specific point described above is actually discussed twice in my ESOP
paper, once informally, and once in a more general setting.  I encourage
you to take a look at that paper for more details.  If you're basing your
knowledge of fundeps on the (now quite outdated) note on my web page, or
on the section of the Hugs manual on which it was based, you may well have
some gaps to fill in.  I'm not too happy with the ESOP paper either; I
couldn't include as much technical material there as I wanted because of
limited s

Re: Problem with functional dependencies

[Marcin 'Qrczak' Kowalczyk]

Thu, 4 Jan 2001 13:01:56 -0800, Mark P Jones <[EMAIL PROTECTED]> pisze:

> I hope now that the problem is becoming clear: this instance
> declaration is not consistent with the dependency; in the first
> two lines above, for example, we see two rows that violate the
> specification because they have the same value of "a", but different
> values for "b" and "c".

I see. So fundeps are not capable of expressing what I hoped, and what
a related but simpler concept I talked about once can express. I wonder
if there are practical uses of fundeps which are not expressible by
this concept.

What I have in mind is the following. A subset of type variables
of a class is chosen. Only that subset is used to find an instance
for resolving constraints with this class. The instance chosen
determines the rest of types. Instances must make this possible,
i.e. be non-unifiable wrt. the active subset of type variables. Voila.

An extended variant: several such subsets instead of one. Probably
each subset should be considered independently, with their results
unified. Or something like that.

This provides an equivalent of types contained in classes in C++.

It does not matter if the passive types in an instance use additional
type variables. This is where fundeps fail.

Having types with type variables which are never instantiated nor
constrained should be equivalent to having ground types!

Why, oh why haven't a more friendly and less problematic concept been
used, instead of fundeps which forever can't be finished in ghc and
have some different semantics in Hugs?

-- 
 __("<  Marcin Kowalczyk * [EMAIL PROTECTED] http://qrczak.ids.net.pl/
 \__/
  ^^  SYGNATURA ZASTÊPCZA
QRCZAK


___
Haskell mailing list
[EMAIL PROTECTED]
http://www.haskell.org/mailman/listinfo/haskell

Yet more on functional dependencies

[George Russell]

I am finding functional dependencies confusing.  (I suspect I am not alone.)
Should the following code work?

class HasConverter a b | a -> b where
   convert :: a -> b

instance (HasConverter a b,Show b) => Show a where
   show value = show (convert value)

___
Haskell mailing list
[EMAIL PROTECTED]
http://www.haskell.org/mailman/listinfo/haskell

Yet more on functional dependencies

[Tom Pledger]

George Russell writes:
 > I am finding functional dependencies confusing.  (I suspect I am not alone.)
 > Should the following code work?
 > 
 > class HasConverter a b | a -> b where
 >convert :: a -> b
 > 
 > instance (HasConverter a b,Show b) => Show a where
 >show value = show (convert value)

Yes.

Let's assume that multi-parameter classes and overlapping instances
are enabled.

Without the functional dependency, the instance decl would be rejected
because the type variable b occurs in the context (HasConverter a b,
Show b) but not in the head (Show a).  The compiler needs to generate
some code for `show value', but it's not allowed to make an arbitrary
substitution for b.

The functional dependency provides a way to determine b uniquely once
a is matched.  So, the compiler can generate the code for `show value'
without being arbitrary.

Regards,
Tom

___
Haskell mailing list
[EMAIL PROTECTED]
http://www.haskell.org/mailman/listinfo/haskell

Re: inference with functional dependencies

[Ken Shan]

On 2001-08-13T18:08:08-0400, Avi Pfeffer wrote:
> Inferring equality between types when there are functional dependencies
> seems to be less powerful than I expected.  Here's a simple example:
> 
> class Eq b => C a b | a -> b
> 
> data T a = forall b . C a b => T b
> data U a = forall b . C a b => U b
> 
> compare :: T a -> U a -> Bool
> compare (T x) (U y) = x == y

Hrm, is it possible for you to define instead

data T a b = C a b => T a b
data U a b = C a b => U a b

and propagate the dependency inference of "a -> b" upward in your
program?  Or even simply say

data T a b = T a b
data U a b = U a b

and put the C constraint further higher up in your program?  Just a
thought...

-- 
Edit this signature at http://www.digitas.harvard.edu/cgi-bin/ken/sig
I saw my inner child once, on a milk carton.

 PGP signature

RE: Syntax of functional dependencies

[Simon Marlow]

> I errorneously specified categories as
> 
> class (Eq object, Eq morphism) => 
>   Category id object morphism | id ->, id -> morphism
>   where  o :: id -> morphism -> morphism -> Maybe morphism
>  dom, cod :: id -> morphism -> object
> 
> it should have been
> 
> class (Eq object, Eq morphism) => 
>   Category id object morphism | id -> object, id -> morphism
>   ... ^^
> 
> - but ghci 5.02.2 does not complain. Why?

The syntax of a functional dependency is (from GHC's parser):

   fd : varids0 '->' varids0

   varids0 
: {- empty -}
| varids0 tyvar

so the list of tyvars on either side of the '->' can be empty.
Functional dependency experts can correct me if I'm wrong, but I imagine
though that 'a ->' is not a very useful functional dependency (isn't it
the same as giving no functional dependency at all?), and '-> a' means
that there can only ever be one instantiation for 'a' in the whole
program.

Cheers,
Simon
___
Haskell mailing list
[EMAIL PROTECTED]
http://www.haskell.org/mailman/listinfo/haskell

A question concerning functional dependencies

[Jerzy Karczmarczuk]

I wanted to write a small package implementing vector spaces,
etc. A part of it is

class Module v s
 where
  (*>) :: s->v->v

defining the multiplication of a vector by a scalar: w = a*>v
Now, as in many other circumstances, concrete vectors are based
on concrete scalars, and I defined really:   class Module v s | v->s  .

One typical instance of vectors is the orthodox functional 
construction

instance Num s => Module (v->s) s 
 where
  (s*>f) x = s * (f x)

and such tests:  u = 2.5 *> sin;   res = u 3.14
pass without tears.

But I wanted also that operators of the type (b->s) -> (b->s),
for example:  inver f = recip . f . recip
be vectors. So:

instance ...=> Module ((v->s)->(v->s)) s
 where
  (s*>op) f = s*>(op f)

But GHCi yells that two instances in view of the functional 
dependency declared are in conflict. Since I believe that 
I do not really understand fundeps in Haskell, and this is not
a GHC 'feature' only, I send this query to the haskell list.
I don't see this conflict. I could remove the fundep, but then
I have other (smaller, but a bit annoying) problems, so I want
to keep it, if only for my own instruction. Good people, help,
please.

Why v [->s]  cannot "coexist" in this context with
 ((v->s)->v) [->s]

Of course all extensions, including overlapping instances are on.

Jerzy Karczmarczuk
Caen, France
___
Haskell mailing list
[EMAIL PROTECTED]
http://www.haskell.org/mailman/listinfo/haskell

Functional dependencies and Constructor Classes

[Martin Sulzmann]

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.

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

RE: Functional dependencies and improvement

[Mark P Jones]

Martin,

| In my previous example I employed FD's to 
| improve constraints. However, there are cases where FD's seem 
| to be overly restrictive.

Yes, of course!  So it will be for any extension of the
type system that retains both decidability and soundness.

The particular form of "improvement" that is provided by FDs
represents an engineering trade off, supporting some useful
examples while requiring only a relatively modest extension
to the syntax and semantics of the language.  They do not
(and were never intended to) provide a universal tool that
can handle all possible refinements of type inference with
classes.

More specialized forms of improvement, including instance
specific rules, have been described elsewhere.  My paper on
improvement [1] provides a framework for this and hints at
some examples.  (In fact I think there is another example
buried in comments in the source code for Hugs that few
people have probably ever seen ... assuming that the
current maintainers haven't had any reason to take it
out!  If you're really curious, look in subst.c ...)

All the best,
Mark

[1]  Simplifying and Improving Qualified Types
 http://www.cse.ogi.edu/~mpj/pubs/improve.html

___
Haskell mailing list
[EMAIL PROTECTED]
http://www.haskell.org/mailman/listinfo/haskell

overlapping instances and functional dependencies

[Wolfgang Jeltsch]

Hello,

I have this code:
class C a b c | a b -> c where
f :: a -> b -> c

instance C a b c => C a (x,y,b) c where
f a (_,_,b) = f a b

instance C a (a,c,b) c where
f _ (_,c,_) = c
ghci -fglasgow-exts -fallow-overlapping-instances compiles it without 
complaint but hugs -98 +o says:
ERROR "ClassProblem.hs":7 - Instances are not consistent with dependencies
*** This instance: C a (a,b,c) b
*** Conflicts with   : C a (b,c,d) e
*** For class: C a b c
*** Under dependency : a b -> c
Can anyone tell me what the reason for this is and, maybe, how to avoid these 
problems with Hugs?

Wolfgang

___
Haskell mailing list
[EMAIL PROTECTED]
http://www.haskell.org/mailman/listinfo/haskell

Functional dependencies interfere with generalization

[Ken Shan]

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:

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


signature.asc
Description: Digital signature
___
Haskell mailing list
[EMAIL PROTECTED]
http://www.haskell.org/mailman/listinfo/haskell

[Haskell] functional dependencies not satisfactory?

[Wolfgang Jeltsch]

Hello,

I came across the following problem:

I define a class with a functional dependency like so:

class C a b | a -> b

Then I want to define a datatype using the fact that the second argument of C 
is dependent on the first:

data C a b => T a = MkT a b

But unfortunately, this doesn’t work, at least not in GHC.

I can try this:

data T a = forall b. C a b => MkT a b

But if I do pattern matching on a value of T a, GHC doesn’t recognize that the 
type of MkT’s second argument is determined by the type of the first.  For 
example, the following function definition is not accepted:

useB :: C a b => T a -> (b -> ()) -> ()
useB (MkT a b) f = f b

In my opinion, the problem is that GHC doesn’t see that because of the 
functional dependency the type exists b. C a b => b is at least as general as 
the type forall b. C a b => b.  Is there a solution to this problem?

Best wishes,
Wolfgang
___
Haskell mailing list
Haskell@haskell.org
http://www.haskell.org/mailman/listinfo/haskell

RE: Yet more on functional dependencies

[Mark P Jones]

| I am finding functional dependencies confusing.  (I suspect I am 
| not alone.)  Should the following code work?
| 
| class HasConverter a b | a -> b where
|convert :: a -> b
| 
| instance (HasConverter a b,Show b) => Show a where
|show value = show (convert value)

It's a separate issue.  There's no reason why a system using
functional dependencies *should* support this.  But it is an
attractive and useful extension that such a system would
probably *want* to include.  (i.e., it's a desirable feature,
not a requirement.)

I typed your example into Hugs on my machine and it seemed to
accept the syntax (which suggests that the implementation is
intended to allow this kind of thing).  But then it choked on
the definition with a curious error message that I suspect is
an indication of a bug in Hugs' treatment of functional
dependencies.  And, for that reason, I'm crossposting this
message to hugs-bugs.  [Let me take the opportunity to remind
good readers of these lists that it is now more than a year
since I retired from the joys of maintaining Hugs, so I'm not
planning to try and track down the source of this bug myself!]
Of course, it could be that my version of Hugs is out of date!

All the best,
Mark


___
Haskell mailing list
[EMAIL PROTECTED]
http://www.haskell.org/mailman/listinfo/haskell

RE: Yet more on functional dependencies

[Simon Peyton-Jones]

| | I am finding functional dependencies confusing.  (I suspect I am 
| | not alone.)  Should the following code work?
| | 
| | class HasConverter a b | a -> b where
| |convert :: a -> b
| | 
| | instance (HasConverter a b,Show b) => Show a where
| |show value = show (convert value)
| 
| It's a separate issue.  There's no reason why a system using
| functional dependencies *should* support this.  But it is an
| attractive and useful extension that such a system would
| probably *want* to include.  (i.e., it's a desirable feature,
| not a requirement.)

There are two things going on here

a) The 'head' of the instance declaration is just "Show a", so this
purports to give an instance declaration for all types "a".  So it
overlaps with other instance declarations, and GHC currently rejects
it for that reason.  (Arguably, if you accept overlapping instance 
declarations, then this should be acceptable too.)

b) There's a "b" in the instance declaration context that doesn't
appear in the head.  This is quite OK, because the functional dependency
ensures that "a" uniquely determines "b".  

So here's a variant that works in the (as-yet-unreleased) GHC 5.0:

data Foo a = MkFoo a

instance (HasConverter a b,Show b) => Show (Foo a) where
show (MkFoo value) = show (convert value)

[Incidentally, functional dependencies don't work at all in GHC 4.08;
don't
even try.]

Simon

___
Haskell mailing list
[EMAIL PROTECTED]
http://www.haskell.org/mailman/listinfo/haskell

Re: Yet more on functional dependencies

[Jeffrey R. Lewis]

Mark P Jones wrote:

> | I am finding functional dependencies confusing.  (I suspect I am
> | not alone.)  Should the following code work?
> |
> | class HasConverter a b | a -> b where
> |convert :: a -> b
> |
> | instance (HasConverter a b,Show b) => Show a where
> |show value = show (convert value)
>
> It's a separate issue.  There's no reason why a system using
> functional dependencies *should* support this.  But it is an
> attractive and useful extension that such a system would
> probably *want* to include.  (i.e., it's a desirable feature,
> not a requirement.)
>
> I typed your example into Hugs on my machine and it seemed to
> accept the syntax (which suggests that the implementation is
> intended to allow this kind of thing).  But then it choked on
> the definition with a curious error message that I suspect is
> an indication of a bug in Hugs' treatment of functional
> dependencies.  And, for that reason, I'm crossposting this
> message to hugs-bugs.  [Let me take the opportunity to remind
> good readers of these lists that it is now more than a year
> since I retired from the joys of maintaining Hugs, so I'm not
> planning to try and track down the source of this bug myself!]
> Of course, it could be that my version of Hugs is out of date!

Could you share the error message please.  Boy, even old maintainers don't know how to 
submit a bug report...  ;-)

Actually, I suspect whatever the problem was has been fixed, because (with -98 +o), it 
compiles fine. (I'm using the bleeding edge, out-of-the-repository version.)

--Jeff


___
Haskell mailing list
[EMAIL PROTECTED]
http://www.haskell.org/mailman/listinfo/haskell

Re: A question concerning functional dependencies

[Ashley Yakeley]

At 2002-09-02 02:46, Jerzy Karczmarczuk wrote:

>class Module v s | v->s  .
...
>instance Num s => Module (v->s) s 
...
>instance ...=> Module ((v->s)->(v->s)) s
...
>But GHCi yells that two instances in view of the functional 
>dependency declared are in conflict.

GHCi is correct. Bear in mind GHC ignores contexts in instance 
declarations when calculating conflicts. This is unfortunate, but 
apparently fixing it would be hard.

((v->s)->(v->s)) is a substitution instance of (v->s). So from the first 
instance,

  instance ...=> Module (v->s) s 

GHC can derive

  instance ...=> Module ((v->s)->(v->s)) (v->s)

...which conflicts with your second instance per the fundep:

  instance ...=> Module ((v->s)->(v->s)) s

The solution of course is to declare new datatypes:

  newtype Vector v s = MkVector (v->s)

  newtype Operator v s = MkOperator ((v->s)->(v->s))

etc.

-- 
Ashley Yakeley, Seattle WA

___
Haskell mailing list
[EMAIL PROTECTED]
http://www.haskell.org/mailman/listinfo/haskell

Re: A question concerning functional dependencies

[Dylan Thurston]

On Mon, Sep 02, 2002 at 03:11:58AM -0700, Ashley Yakeley wrote:
> At 2002-09-02 02:46, Jerzy Karczmarczuk wrote:
> 
> >class Module v s | v->s  .
> ...
> >instance Num s => Module (v->s) s 
> ...
> >instance ...=> Module ((v->s)->(v->s)) s
> ...
> >But GHCi yells that two instances in view of the functional 
> >dependency declared are in conflict.
> 
> GHCi is correct. Bear in mind GHC ignores contexts in instance 
> declarations when calculating conflicts. This is unfortunate, but 
> apparently fixing it would be hard.

Even taking contexts into account, these two might still conflict: if
you had

instance Num ((v->s)->v)

for some values of v and s, you would get a conflict.

GHC (and Hugs) check for potential conflicts like this unless you
explicitly allow overlapping instances.

--Dylan



msg11456/pgp0.pgp
Description: PGP signature

Re: A question concerning functional dependencies

[Ashley Yakeley]

At 2002-09-02 07:47, Dylan Thurston wrote:

>GHC (and Hugs) check for potential conflicts like this unless you
>explicitly allow overlapping instances.

AFAIK, even with overlapping instances allowed, GHC will still complain 
if there's a fundep.

See 
.

-- 
Ashley Yakeley, Seattle WA

___
Haskell mailing list
[EMAIL PROTECTED]
http://www.haskell.org/mailman/listinfo/haskell

Re: Functional dependencies and Constructor Classes

[Yoann Padioleau]

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

[Martin Sulzmann]

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

[Mark P Jones]

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 and Constructor Classes

[Yoann Padioleau]

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]

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: overlapping instances and functional dependencies

[Andrew J Bromage]

G'day all.

On Sat, Aug 09, 2003 at 01:32:49AM +0200, Wolfgang Jeltsch wrote:

> ghci -fglasgow-exts -fallow-overlapping-instances compiles it without 
> complaint

If it helps, ghci will complain the first time you actually try to use
it.

Cheers,
Andrew Bromage
___
Haskell mailing list
[EMAIL PROTECTED]
http://www.haskell.org/mailman/listinfo/haskell

RE: overlapping instances and functional dependencies

[Hal Daume]

Suppose somewhere we have an instance:

 instance C Int Bool Int

when the first instance decl you have says we also have

  instance C Int (x,y,Bool) Int

in this case, Int + (x,y,Bool) should uniq. specify Int.

however, we also have:

  instance C a (a,c,b) c

where, if we let a=Int, b=Bool, c=Char, then we get that
  Int + (Int,Char,Bool) should uniq. specify Char.

these two confict because if, in the first case, we instantiate x to Int
and y to Char, then one says that the third param should be a Bool and
the other says the third param should be a Char.

(or at least this is my understanding -- someone might correct me)

 - Hal

 --
 Hal Daume III   | [EMAIL PROTECTED]
 "Arrest this man, he talks in maths."   | www.isi.edu/~hdaume


> -Original Message-
> From: [EMAIL PROTECTED] 
> [mailto:[EMAIL PROTECTED] On Behalf Of Wolfgang Jeltsch
> Sent: Friday, August 08, 2003 4:33 PM
> To: The Haskell Mailing List
> Subject: overlapping instances and functional dependencies
> 
> 
> Hello,
> 
> I have this code:
> class C a b c | a b -> c where
> f :: a -> b -> c
> 
> instance C a b c => C a (x,y,b) c where
> f a (_,_,b) = f a b
> 
> instance C a (a,c,b) c where
> f _ (_,c,_) = c
> ghci -fglasgow-exts -fallow-overlapping-instances compiles it without 
> complaint but hugs -98 +o says:
> ERROR "ClassProblem.hs":7 - Instances are not consistent 
> with dependencies
> *** This instance: C a (a,b,c) b
> *** Conflicts with   : C a (b,c,d) e
> *** For class: C a b c
> *** Under dependency : a b -> c
> Can anyone tell me what the reason for this is and, maybe, 
> how to avoid these 
> problems with Hugs?
> 
> Wolfgang
> 
> ___
> Haskell mailing list
> [EMAIL PROTECTED]
> http://www.haskell.org/mailman/listinfo/haskell
> 
___
Haskell mailing list
[EMAIL PROTECTED]
http://www.haskell.org/mailman/listinfo/haskell

Re: overlapping instances and functional dependencies

[Wolfgang Jeltsch]

I wrote on Saturday, 2003-08-09, 01:32, CEST:
> Hello,
>
> I have this code:
> class C a b c | a b -> c where
> f :: a -> b -> c
>
> instance C a b c => C a (x,y,b) c where
> f a (_,_,b) = f a b
>
> instance C a (a,c,b) c where
> f _ (_,c,_) = c
> ghci -fglasgow-exts -fallow-overlapping-instances compiles it without
> complaint but hugs -98 +o says:
> ERROR "ClassProblem.hs":7 - Instances are not consistent with
> dependencies
> *** This instance: C a (a,b,c) b
> *** Conflicts with   : C a (b,c,d) e
> *** For class: C a b c
> *** Under dependency : a b -> c
> Can anyone tell me what the reason for this is and, maybe, how to avoid
> these problems with Hugs?
>
> Wolfgang

Hal Daume answered on Saturday, 2003-08-09, 01:53, CEST:
> Suppose somewhere we have an instance:
>
>  instance C Int Bool Int
>
> when the first instance decl you have says we also have
>
>   instance C Int (x,y,Bool) Int
>
> in this case, Int + (x,y,Bool) should uniq. specify Int.
>
> however, we also have:
>
>   instance C a (a,c,b) c
>
> where, if we let a=Int, b=Bool, c=Char, then we get that
>   Int + (Int,Char,Bool) should uniq. specify Char.
>
> these two confict because if, in the first case, we instantiate x to Int and
> y to Char, then one says that the third param should be a Bool and the other
> says the third param should be a Char.
>
> (or at least this is my understanding -- someone might correct me)
>
>  - Hal

Hello,

I wouldn't suppose that there is a conflict in your example. The question is 
for which t there is an instance C Int (Int,Char,Bool) t. There are two 
competing instance declarations:
(1) instance C a b c => C a (x,y,b) c [...]
Because in your example there is an instance C Int Bool Int we would
get the instance C Int (Int,Char,Bool) Int.
(2) instance C a (a,c,b) c [...]
This clearly votes for C Int (Int,Char,Bool) Char.
But the second instance declaration is more specific. In the first one we have 
the "pattern" "arbitrary type - triple type - arbitrary type" with no further 
restrictions. In the second one we have the same "pattern" but with the 
restriction that the first parameter must equal the type of the first triple 
element and the third parameter must equal the type of the second triple 
element. Because of the handling of overlapping instances, the compiler 
should take the second instance declaration and deduce the instance C Int 
(Int,Char,Bool) Char.

What's wrong with my interpretation?

Wolfgang

___
Haskell mailing list
[EMAIL PROTECTED]
http://www.haskell.org/mailman/listinfo/haskell

Re: overlapping instances and functional dependencies

[Wolfgang Jeltsch]

Hello,

I think, I realized now what my mistake was. The handling of overlapping 
instances comes into play when the compiler has to decide which method 
definition to choose for a specific instance. It is not for choosing one of 
more possible instances.

In my example, C Int (Int,Char,Bool) Int and C Int (Int,Char,Bool) Char where 
both candidates for instances of C. Because they match the pattern of the 
first instance declaration (which is the more general one), both candidates 
actually have to be instances. The handling of overlapping instances only 
states that the compiler has to use the method definitions of the second 
instance declaration for the instance C (Int,Char,Bool) Char.

Am I correct?

Wolfgang


On Monday, 2003-08-18, 00:37, CEST, Wolfgang Jeltsch wrote:
> I wrote on Saturday, 2003-08-09, 01:32, CEST:
> > Hello,
> >
> > I have this code:
> > class C a b c | a b -> c where
> > f :: a -> b -> c
> >
> > instance C a b c => C a (x,y,b) c where
> > f a (_,_,b) = f a b
> >
> > instance C a (a,c,b) c where
> > f _ (_,c,_) = c
> > ghci -fglasgow-exts -fallow-overlapping-instances compiles it without
> > complaint but hugs -98 +o says:
> > ERROR "ClassProblem.hs":7 - Instances are not consistent with
> > dependencies
> > *** This instance: C a (a,b,c) b
> > *** Conflicts with   : C a (b,c,d) e
> > *** For class: C a b c
> > *** Under dependency : a b -> c
> > Can anyone tell me what the reason for this is and, maybe, how to avoid
> > these problems with Hugs?
> >
> > Wolfgang
>
> Hal Daume answered on Saturday, 2003-08-09, 01:53, CEST:
> > Suppose somewhere we have an instance:
> >
> >  instance C Int Bool Int
> >
> > when the first instance decl you have says we also have
> >
> >   instance C Int (x,y,Bool) Int
> >
> > in this case, Int + (x,y,Bool) should uniq. specify Int.
> >
> > however, we also have:
> >
> >   instance C a (a,c,b) c
> >
> > where, if we let a=Int, b=Bool, c=Char, then we get that
> >   Int + (Int,Char,Bool) should uniq. specify Char.
> >
> > these two confict because if, in the first case, we instantiate x to Int
> > and y to Char, then one says that the third param should be a Bool and
> > the other says the third param should be a Char.
> >
> > (or at least this is my understanding -- someone might correct me)
> >
> >  - Hal
>
> Hello,
>
> I wouldn't suppose that there is a conflict in your example. The question
> is for which t there is an instance C Int (Int,Char,Bool) t. There are two
> competing instance declarations:
> (1) instance C a b c => C a (x,y,b) c [...]
> Because in your example there is an instance C Int Bool Int we
> would get the instance C Int (Int,Char,Bool) Int.
> (2) instance C a (a,c,b) c [...]
> This clearly votes for C Int (Int,Char,Bool) Char.
> But the second instance declaration is more specific. In the first one we
> have the "pattern" "arbitrary type - triple type - arbitrary type" with no
> further restrictions. In the second one we have the same "pattern" but with
> the restriction that the first parameter must equal the type of the first
> triple element and the third parameter must equal the type of the second
> triple element. Because of the handling of overlapping instances, the
> compiler should take the second instance declaration and deduce the
> instance C Int (Int,Char,Bool) Char.
>
> What's wrong with my interpretation?
>
> Wolfgang

___
Haskell mailing list
[EMAIL PROTECTED]
http://www.haskell.org/mailman/listinfo/haskell

Re: overlapping instances and functional dependencies

[oleg]

Wolfgang Jeltsch has observed:
> I have this code:
> class C a b c | a b -> c where
> f :: a -> b -> c
>
> instance C a b c => C a (x,y,b) c where
> f a (_,_,b) = f a b
>
> instance C a (a,c,b) c where
> f _ (_,c,_) = c
> ghci -fglasgow-exts -fallow-overlapping-instances compiles it without
> complaint but hugs -98 +o says:
> ERROR "ClassProblem.hs":7 - Instances are not consistent with
> dependencies
> *** This instance: C a (a,b,c) b
> *** Conflicts with   : C a (b,c,d) e
> *** For class: C a b c
> *** Under dependency : a b -> c
> Can anyone tell me what the reason for this is and, maybe, how to avoid
> these problems with Hugs?

I believe it's helpful to think about this problem in terms of logical
programming, and proceed in phases.

Phase 1. The compiler sees the instances of a class C and compiles
them into a database of instances. In Prolog terms, given the
instances

instance C a b c => C a (x,y,b) c
instance C a (a,c,b) c

the compiler asserts

c(A,tuple(A,C,B),C,dict2).
c(A,tuple(X,Y,B),C,dict1) :- c(A,B,C,_).

In Haskell, lower-case type identifiers are variables and upper-case
one are type constants. In Prolog, it's the other way around:
lower-cased identifiers are constants and upper-cased are variables. I
hope that won't cause too much confusion.

I happen to have SWI-Prolog handy, in which I assert the above two
facts.

Phase 2. Suppose the compiler sees a type with a class constraint ``C Int
(Int,Char,Bool) t'' The compiler can determine the appropriate instance
by issuing a query:

?- bagof(Dict,c(int,tuple(int,char,bool),T,Dict),Dicts).

Dict = _G158
T = char
Dicts = [dict2] 
Yes

In our case, only one instance matched, and we found the corresponding
dictionary. If Dicts were a list of two or more dictionaries, we would
have needed to choose the most specific, if any.

Phase 1a.
Before we get to Phase 2 however, we have to take care of one more
problem. The class declaration specified a dependency:
class C a b c | a b -> c

which all members of that class must satisfy. The instances (which
define the membership) must be consistent with the dependency "a b -> c".
The consistency would be violated if there were two types "C a b c1"
and "C a b c2" such that c1 /== c2. Thus we can check the
consistency of the instances by searching for a counter-example:

?- c(A,B,C1,_), c(A,B,C2,_), \+ C1 == C2.

A = _G151
B = tuple(_G151, _G153, tuple(_G151, _G158, _G302))
C1 = _G153
C2 = _G158 
Yes

Alas, in this case we found a counter-example: types
C a (a,c,(a,c',d)) c
C a (a,c,(a,c',d)) c'

with c' /= c match some instance but contradict the functional
dependency. Therefore, the compiler complaints.



___
Haskell mailing list
[EMAIL PROTECTED]
http://www.haskell.org/mailman/listinfo/haskell

Re: overlapping instances and functional dependencies

[C T McBride]

Hi all

With overlapping instances, I'm allowed

  class OK x y

  instance Functor f => OK (f x) (f y)

  instance Functor f => OK x (f y)

but I'm not allowed

  class Bad x y z | x y -> z

  instance Functor f => Bad (f x) (f y) Bool

  instance Functor f => Bad x (f y) Int

I don't quite see why. Naively, I imagine that if the OK instances are
effectively prioritized, then Bad's rules for computing z from x and y
could be similarly prioritized. Can anyone explain why this naive
imagining is incorrect?

Cheers

Conor

PS a more complicated, less contrived example is available on request
___
Haskell mailing list
[EMAIL PROTECTED]
http://www.haskell.org/mailman/listinfo/haskell

Re: overlapping instances and functional dependencies

[Tom Pledger]

C T McBride writes:
 :
 | but I'm not allowed
 | 
 |   class Bad x y z | x y -> z
 | 
 |   instance Functor f => Bad (f x) (f y) Bool
 | 
 |   instance Functor f => Bad x (f y) Int
 | 
 | I don't quite see why. Naively, I imagine that if the OK instances are
 | effectively prioritized, then Bad's rules for computing z from x and y
 | could be similarly prioritized. Can anyone explain why this naive
 | imagining is incorrect?

Hi.

The first instance decl includes

instance Bad [()] [()] Bool

and the second includes

instance Bad [()] [()] Int

which break the functional dependency because x and y do not uniquely
determine z.

But I suspect you already knew that, and were asking why the
functional dependency feature is based on uniqueness constraints, not
prioritised type-computation rules.  I'm not sure of the original
reason, but the uniqueness approach supports some neat tricks

http://www.willamette.edu/~fruehr/haskell/evolution.html#fundep

which the prioritised approach probably wouldn't.

Regards,
Tom

___
Haskell mailing list
[EMAIL PROTECTED]
http://www.haskell.org/mailman/listinfo/haskell

RE: overlapping instances and functional dependencies

[Simon Peyton-Jones]

| class C a b c | a b -> c where
| f :: a -> b -> c
| 
| instance C a b c => C a (x,y,b) c where
| f a (_,_,b) = f a b
| 
| instance C a (a,c,b) c where
| f _ (_,c,_) = c
| ghci -fglasgow-exts -fallow-overlapping-instances compiles it without
| complaint but hugs -98 +o says:
| ERROR "ClassProblem.hs":7 - Instances are not consistent with
dependencies
| *** This instance: C a (a,b,c) b
| *** Conflicts with   : C a (b,c,d) e
| *** For class: C a b c
| *** Under dependency : a b -> c

There are several things going on here.

1.  The functional dependency (a b -> c), together with an instance
declaration
instance C   
means that 
if you have a constraint (C   ), 
and  matches 
and  matches 
then
 must look like 

Here "matches" means "is a substitution instance of".

Mark Jones's original paper specified that 
the free variables of  must be a subset of 
the free variable of  and 

Reason: then the matching of  and  generates a substitution that
covers all the free variables of , and then " must look like
" means exactly that " must be the same as  instantiated by
the matches of / and /".

However, it seems that neither Hugs nor GHC make this test, which is
very naughty of them

2.  Having omitted this test, Hugs is complaining that a constraint
C Int (Int,Bool,Bool) 
would match both instance declarations, so it's not sure which  to
make  equal to.  I could check why GHC does not complain, but it may
be that the answer is the same in both cases (namely the unbound 'c').


3.  None of this has to do with overlapping instances per se.




I'm working with Martin Sulzmann on some ideas for loosening the
restriction (1) above, but it's all a bit vacuous in your example.  What
is the fundep is buying you?  It doesn't convey any information to say
that " must look like c", if c is completely unbound!

Simon

___
Haskell mailing list
[EMAIL PROTECTED]
http://www.haskell.org/mailman/listinfo/haskell

RE: overlapping instances and functional dependencies

[Simon Peyton-Jones]

| With overlapping instances, I'm allowed
| 
|   class OK x y
| 
|   instance Functor f => OK (f x) (f y)
| 
|   instance Functor f => OK x (f y)
| 
| but I'm not allowed
| 
|   class Bad x y z | x y -> z
| 
|   instance Functor f => Bad (f x) (f y) Bool
| 
|   instance Functor f => Bad x (f y) Int
| 
| I don't quite see why. Naively, I imagine that if the OK instances are
| effectively prioritized, then Bad's rules for computing z from x and y
| could be similarly prioritized. Can anyone explain why this naive
| imagining is incorrect?

I don't think anyone has really worked through the interaction of
overlapping instances (already swampy) with functional dependencies.
What you say makes sense, but it's not what GHC or Hugs implement.
Maybe they should

Simon


___
Haskell mailing list
[EMAIL PROTECTED]
http://www.haskell.org/mailman/listinfo/haskell

Re: Functional dependencies interfere with generalization

[Brandon Michael Moore]

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

[Ken Shan]

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'. (

Re: [Haskell] functional dependencies not satisfactory?

[Stefan O'Rear]

On Tue, Sep 04, 2007 at 06:20:26PM +0200, Wolfgang Jeltsch wrote:
> Hello,
> 
> I came across the following problem:
> 
> I define a class with a functional dependency like so:
> 
> class C a b | a -> b
> 
> Then I want to define a datatype using the fact that the second argument of C 
> is dependent on the first:
> 
> data C a b => T a = MkT a b
> 
> But unfortunately, this doesn’t work, at least not in GHC.
> 
> I can try this:
> 
> data T a = forall b. C a b => MkT a b
> 
> But if I do pattern matching on a value of T a, GHC doesn’t recognize that 
> the 
> type of MkT’s second argument is determined by the type of the first.  For 
> example, the following function definition is not accepted:
> 
> useB :: C a b => T a -> (b -> ()) -> ()
> useB (MkT a b) f = f b
> 
> In my opinion, the problem is that GHC doesn’t see that because of the 
> functional dependency the type exists b. C a b => b is at least as general as 
> the type forall b. C a b => b.  Is there a solution to this problem?

And so yet another person discovers why functional dependancies are
Bad(tm) - the semantics generated by their typing derivations do not
correspond to the naïve model.

In particular, functional dependencies serve *only* to avoid ambiguity;
they cannot be used to satisfy equality constraints.

Type synonym families, the proposed alternative to functional
dependencies, can handle this well:

{-# LANGUAGE TypeFamilies #-}

class C a where
type B a :: *

data C a => T a = MkT a (B a)

useB :: C a => T a -> (B a -> ()) -> ()
useB (MkT a b) f = f b

It should be emphasized that this program worked the very first time I
typed it in.  No back-and-forth arguing with the checker!

Stefan



signature.asc
Description: Digital signature
___
Haskell mailing list
Haskell@haskell.org
http://www.haskell.org/mailman/listinfo/haskell

Re: [Haskell] functional dependencies not satisfactory?

[Wolfgang Jeltsch]

Am Dienstag, 4. September 2007 22:00 schrieben Sie:
> […]

> It should be emphasized that this program worked the very first time I
> typed it in.

Which version of GHC are you using?  I’m a bit confused since the latest 
successful nightly build for i386-unknown-linux seems to be from August 20.  
Are type families already implemented in this version?  Was there any change 
in type family support since then?

Best wishes,
Wolfgang
___
Haskell mailing list
Haskell@haskell.org
http://www.haskell.org/mailman/listinfo/haskell

Re: [Haskell] functional dependencies not satisfactory?

[Stefan O'Rear]

On Tue, Sep 04, 2007 at 11:11:00PM +0200, Wolfgang Jeltsch wrote:
> Am Dienstag, 4. September 2007 22:00 schrieben Sie:
> > […]
> 
> > It should be emphasized that this program worked the very first time I
> > typed it in.
> 
> Which version of GHC are you using?  I’m a bit confused since the latest 
> successful nightly build for i386-unknown-linux seems to be from August 20.  
> Are type families already implemented in this version?  Was there any change 
> in type family support since then?

Type synonym families were only merged on the 28th IIRC.

[EMAIL PROTECTED]:~$ ghci -V
The Glorious Glasgow Haskell Compilation System, version 6.7.20070829

Stefan


signature.asc
Description: Digital signature
___
Haskell mailing list
Haskell@haskell.org
http://www.haskell.org/mailman/listinfo/haskell

Re: [Haskell] functional dependencies not satisfactory?

[Manuel M T Chakravarty]

Wolfgang Jeltsch wrote,

I came across the following problem:

I define a class with a functional dependency like so:

class C a b | a -> b

Then I want to define a datatype using the fact that the second argument of C 
is dependent on the first:


data C a b => T a = MkT a b

But unfortunately, this doesn’t work, at least not in GHC.

I can try this:

data T a = forall b. C a b => MkT a b

But if I do pattern matching on a value of T a, GHC doesn’t recognize that the 
type of MkT’s second argument is determined by the type of the first.  For 
example, the following function definition is not accepted:


useB :: C a b => T a -> (b -> ()) -> ()
useB (MkT a b) f = f b

In my opinion, the problem is that GHC doesn’t see that because of the 
functional dependency the type exists b. C a b => b is at least as general as 
the type forall b. C a b => b.  Is there a solution to this problem?


You may want to have a look at Section 2.3 of "System F with Type 
Equality Coercions" 
<http://www.cse.unsw.edu.au/~chak/papers/SCPD07.html>, which 
explains why GHC rejects the program.


The mentioned paper also outlines an alternative translation of FDs 
using System FC that does not suffer from this problem. 
Unfortunately, it is not quite clear how to extend type checking for 
FDs in such a way that the required System FC coercion-evidence 
types are produced by the type checker.


This is one of the reasons why I believe that we should use the type 
families mentioned by Stefan instead of functional dependencies. 
Type checker support for type synonym families (the flavour needed 
for your example) has been merged into GHC's development version a 
week ago.  For more details, see


  http://haskell.org/haskellwiki/GHC/Type_families

Manuel
___
Haskell mailing list
Haskell@haskell.org
http://www.haskell.org/mailman/listinfo/haskell

Re: Multiparameter class confusion (and functional dependencies)

[Graham Klyne]

At 02:18 07/06/03 +0200, Dylan Thurston wrote:

On Wed, Jun 04, 2003 at 01:21:00PM +0100, Graham Klyne wrote:
> There is a recurring difficulty I'm having using multiparameter classes.
>=20
> Most recently, I have a class Rule:
> [[
> class (Expression ex, Eq (rl ex)) =3D> Rule rl ex where
>   ...
> ]]
>=20
> Which I wish to instantiate for a type GraphClosure via something like:
> [[
> instance (Label lb, LDGraph lg lb) =3D> Expression (lg lb) where
>   ...
>=20
> data (Label lb, LDGraph lg lb) =3D> GraphClosure lg lb =3D ...
>=20
> instance Rule GraphClosure (NSGraph RDFLabel) where
>   ...
>=20
> ]]
> ...
> I think that what I really *want* to do here is change the kind of=20
> GraphClosure to be (* -> *) rather than (* -> * -> *).  But if I try this:
>=20
> [[
> data (Label lb, LDGraph lg lb) =3D> GraphClosure (lg lb) =3D ...
> ]]
> a syntax error is reported by Hugs and GHC.
You haven't quite shown enough of your code.  One thing you might
consider is dropping the context from the definition of the
GraphClosure type.  Class contexts in data declarations end up being
largely useless, anyway, since the dictionary is never actually used
for anything.  (There was a thread a few years ago about this.)
You could then write
> data GraphClosure lglb =3D ...

But this only works if the definition of GraphClosure only uses (lg
lb), not the individual pieces.
I'm still wrestling with the exact form of the code, and it's part of a 
much larger program in development.  I reproduce more of the code below, 
but I suspect you may be right in that I'm including unnecessary context in 
the data declaration(s).

After writing my original message, I also spotted something in the 
implementation of Control.Monad.State, in which:
[[
class (Monad m) => MonadState s m | m -> s where
  get :: m s
  put :: s -> m ()
]]
has 's' being declared as determined by m, without explicitly saying 
how.  I haven't yet really learned about functional dependencies...

[ ... wanders off to read paper [1] on functional dependencies ... ]

... they do seem to shed some light on the issue, if only to indicate that 
I've been mis-reading the multiparameter class construct.  For some reason, 
I've been reading it so that, say, (C a b) means that (a b) is an instance 
of C, where it seems that I should be reading is to mean (a,b) are in some 
relation C.  And, if I've got it right, each instantiation of C potentially 
extends the relation (a,b) defined by C.

A supplementary musing:  suppose I have:
class X a b c d | (a,b) -> (c,d)
then among all the instances of D, the combination D a b _ _ must appear at 
most once for any given a and b?

I think this is beginning to make more sense, but I've yet to go figure how 
it affects my code.  (Maybe this will make the magic seem less black for me?)

#g
--
[1] http://www.cse.ogi.edu/~mpj/pubs/fundeps-esop2000.pdf

Below is an larger excerpt from the (unfinished) code I'm working 
on.  Based on your comments, I think I can lose the context (and the 'lg' 
references) from 'GraphClosure'.  Maybe there are similar changes I can 
make to the definition of LDGraph (which I already know should be reviewed).

The following two classes are intended to provide some base components of a 
generic inference-verification (proof) framework:
[[
-- |Expression is a type class for values over which proofs
--  may be constructed.
class (Eq ex) => Expression ex where
-- |Is expression true in all interpretations?
--  If so, then its truth is assumed without justification.
isValid :: ex -> Bool

-- |Rule is a type class for inference rules that can be used
--  to construct a step in a proof.
class (Expression ex, Eq (rl ex)) => Rule rl ex where
-- |Name of rule, for use when displaying a proof
ruleName :: rl ex -> String
-- |Forward application of a rule, takes a list of
--  expressions and returns a list (possibly empty)
--  of forward applications of the rule to combinations
--  of the antecedent expressions.
fwdApply :: rl ex -> [ex] -> [ex]
-- |Backward application of a rule, takes an expression
--  and returns a list of antecedent expressions that
--  jointly yield the given expression through application
--  of the inference rule.
bwdApply :: rl ex -> ex -> [ex]
]]
And here are my attempts to instantiate these classes for a generic class 
of directed labelled graphs (LDGraph) over some node-label type lb:
[[
-- |Instances of LDGraph are also instance of the
--  Expression class, for which proofs can be constructed.
--  The empty RDF graph is always True (other enduring
--  truths are asserted as axioms).
instance (Label lb, LDGraph lg lb) => Expression (lg lb) where
isValid gr = null $ getArcs gr

[Haskell] Re: Functional dependencies interfere with generalization

[oleg]

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 = No

[Haskell] Functional dependencies and type inference (2)

[Louis-Julien Guillemette]

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:


class CpsForm a b | a -> b
instance CpsForm Bool Bool

A natural formulation of the type of the CPS transformation would be

cps :: CpsForm t cps_t => Term t -> (Term cps_t -> Term ()) -> Term ()

cps (B b) c = c (B b)  -- doesn't type-check!
cps (Cnd p q r) c = cps p (\p' -> Cnd p' (cps q c) (cps r c))
   -- type-checks OK

but the first clause of the function doesn't type-check:

Couldn't match the rigid variable `cps_t' against `Bool'
  `cps_t' is bound by the type signature for `cps'
  Expected type: Term cps_t
  Inferred type: Term Bool
In the application `B b'
In the first argument of `c', namely `(B b)'


On the contrary, if we push the (otherwise implicit) quantifier inside the 
parentheses:


cps' :: Term t
   -> (forall cps_t . CpsForm t cps_t => Term cps_t -> Term ())
   -> Term ()

cps' (B b) c = c (B b)  -- type-checks OK
cps' (Cnd p q r) c = cps' p (\p' -> Cnd p' (cps' q c) (cps' r c))
-- doesn't type-check!

then the second clause fails to type-check:

Couldn't match the rigid variable `cps_t' against `Bool'
  `cps_t' is bound by the polymorphic type `forall cps_t.
(CpsForm t cps_t) =>
Term cps_t -> Term ()'
  Expected type: Term Bool
  Inferred type: Term cps_t
In the first argument of `Cnd', namely `p''
In a lambda abstraction: \ p' -> Cnd p' (cps' q c) (cps' r c)

This case seems to be an instance of a problem discussed earlier.
(http://www.haskell.org/pipermail/haskell-cafe/2005-August/011053.html)

Any suggestion on a way to get around this problem in current Haskell?

And, any hope to get this fixed in a future release of GHC?

Thanks

Louis-Julien
___
Haskell mailing list
Haskell@haskell.org
http://www.haskell.org/mailman/listinfo/haskell

Functional Dependencies (Was RE: Dimensional analysis with fundeps)

[Mark P Jones]

Dear All,

| 1) What is a fundep?

Fundeps are "functional dependencies", which have long been used to
specify constraints on the tables used in relational databases.  In
the current context, people are using "fundeps" to refer to the way
that this idea has been adapted to work with multiple parameter type
classes.  My paper on this subject was presented at ESOP last year,
but the publishers asked me not to distribute the paper electronically
until a year after the conference.  Now that year has passed, and
I am happy to make the paper available:

  http://www.cse.ogi.edu/~mpj/pubs/fundeps-esop2000.pdf

Note that, for reasons of space, I wasn't able to include all the
technical details of the type system in the paper.  If you are
interested in such details, or you are looking for more background,
then you might want to check out my earlier work on "Simplifying
and Improving Qualified Types", which is available from:

  http://www.cse.ogi.edu/~mpj/pubs/improve.html

All the best,
Mark


___
Haskell mailing list
[EMAIL PROTECTED]
http://www.haskell.org/mailman/listinfo/haskell

[Haskell] generic currying (type classes and functional dependencies)

[Duncan Coutts]

Hi All,

I'm trying to write a generic curry (& uncurry) function that works for
functions of any arity. I have a couple solutions that nearly work, both
involving type classes.

Here's the first one:

class Curry tupled curried where
  genericCurry   :: tupled -> curried
  genericUncurry :: curried -> tupled

The base case is obvious:

instance Curry ((a,b) -> c) (a -> b -> c) where
  genericCurry   f   x y  = f (x,y)
  genericUncurry f' (x,y) = f' x y

However, the inductive case is more tricky. We cannot generically create
tuples of arbitrary size so we'll have to make do with left (or right)
nested pairs. This nesting leads to problems later and for starters
requires overlapping instances:

instance Curry (   (b,c)  -> d) ( b -> c -> d) =>
 Curry ((a,(b,c)) -> d) (a -> b -> c -> d) where
  genericCurry   f  a  b c   = f (a,(b,c))
  genericUncurry f (a,(b,c)) = f  a  b c

This works, but when we come to use it we often run into cases where the
type checker complains with messages such as:
No instance for (Curry ((Int, Int) -> Int) (a -> b -> Int))
I guess that this is because it fails to be able to convince itself that
a & b are Int, in which case there would be an instance. This can be
solved by supplying enough type annotations, however this is annoying
and part of the point of a generic curry is that we don't know the arity
of the function to which we are applying it.

So I thought that functional dependencies might help because the curried
type should uniquely determine the uncurried type (and vice versa).
However if I change the class declaration to:

class Curry tupled curried | tupled -> curried, curried -> tupled  where
  genericCurry   :: tupled -> curried
  genericUncurry :: curried -> tupled

Then the compiler complains about my instance declarations:

Functional dependencies conflict between instance declarations:
  ./Curry.hs:11:0: instance Curry ((a, b) -> c) (a -> b -> c)
  ./Curry.hs:16:0:
instance (Curry ((b, c) -> d) (b -> c -> d)) =>
 Curry ((a, (b, c)) -> d) (a -> b -> c -> d)

I don't fully understand why this is the case, but it is to do with the
nested pairing, because individual instance declarations for 3-tuples,
4-tuples work find.

Any insight or suggestions would be interesting.

Duncan

___
Haskell mailing list
[EMAIL PROTECTED]
http://www.haskell.org/mailman/listinfo/haskell

Re: [Haskell] Functional dependencies and type inference (2)

[kahl]

 Louis-Julien Guillemette <[EMAIL PROTECTED]> 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:
 > 
 > class CpsForm a b | a -> b
 > instance CpsForm Bool Bool
 > 
 > A natural formulation of the type of the CPS transformation would be
 > 
 > cps :: CpsForm t cps_t => Term t -> (Term cps_t -> Term ()) -> Term ()
 > 
[...]
 >  Couldn't match the rigid variable `cps_t' against `Bool'
[...]
 > 
 > This case seems to be an instance of a problem discussed earlier.
 > (http://www.haskell.org/pipermail/haskell-cafe/2005-August/011053.html)
 > 
 > Any suggestion on a way to get around this problem in current Haskell?
 > 

My way around this is to replace instance derivations by GADT elements,
something like:

data CpsForm :: * -> * -> * where
  CpsBool :: CpsForm Bool Bool

cps :: CpsForm t cps_t -> Term t -> (Term cps_t -> Term ()) -> Term ()


YMMV!


Wolfram
___
Haskell mailing list
Haskell@haskell.org
http://www.haskell.org/mailman/listinfo/haskell

[Haskell] Re: Functional dependencies and type inference (2)

[oleg]

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

[Haskell] Re: Functional dependencies and type inference (2)

[Stefan Monnier]

> 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)

[oleg]

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)

[Stefan Monnier]

>> > 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

Re: [Haskell] generic currying (type classes and functional dependencies)

[Ronny Wichers Schreur]

Duncan Coutts writes (to the Haskell Mailing list):

I'm trying to write a generic curry (& uncurry) function that works for
functions of any arity.
See 
where oleg presents a (ghc-specific) solution.
Cheers,

Ronny Wichers Schreur
___
Haskell mailing list
[EMAIL PROTECTED]
http://www.haskell.org/mailman/listinfo/haskell

Re: [Haskell] generic currying (type classes and functional dependencies)

[Malcolm Wallace]

Duncan Coutts <[EMAIL PROTECTED]> writes:

> So I thought that functional dependencies might help because the curried
> type should uniquely determine the uncurried type (and vice versa).
> However if I change the class declaration to:
> 
> class Curry tupled curried | tupled -> curried, curried -> tupled  where
>   genericCurry   :: tupled -> curried
>   genericUncurry :: curried -> tupled
> 
> Then the compiler complains about my instance declarations:
> 
> Functional dependencies conflict between instance declarations:
>   ./Curry.hs:11:0: instance Curry ((a, b) -> c) (a -> b -> c)
>   ./Curry.hs:16:0:
> instance (Curry ((b, c) -> d) (b -> c -> d)) =>
>  Curry ((a, (b, c)) -> d) (a -> b -> c -> d)
> 
> I don't fully understand why this is the case, but it is to do with the
> nested pairing, because individual instance declarations for 3-tuples,
> 4-tuples work fine.

With a little alpha-renaming:

instance Curry ((a, b) -> c) (a -> b -> c)

instance (Curry ((e, f) -> g) (e -> f -> g)) =>
  Curry ((d, (e, f)) -> g) (d -> e -> f -> g)

It should be fairly easy to see that the type
  (d, (e, f)) -> g
is an instance of
  (a, b) -> c
where a==d and b==(e,f) and c==g.  Also
  (d -> e -> f -> g)
is an instance of
  (a -> b -> c)
where a=d and b==e and c==(f->g).  So for one thing your two instances
overlap, but additionally, the type-variables do not unify, because
in the tupled part of the Curry predicate, b==(e,f), but in the curried
part of the predicate, b==e.

Regards,
Malcolm
___
Haskell mailing list
[EMAIL PROTECTED]
http://www.haskell.org/mailman/listinfo/haskell

Re: [Haskell] generic currying (type classes and functional dependencies)

[Esa Pulkkinen]

In message <[EMAIL PROTECTED]>, Duncan Coutts writes:
>I'm trying to write a generic curry (& uncurry) function that works for
>functions of any arity. I have a couple solutions that nearly work, both
>involving type classes.
[SNIP]
>Any insight or suggestions would be interesting.

Here's one solution, which I think is more general than what you ask,
but I guess it should work as well. It's based on adjunctions from
category theory:

class (Functor path, Functor space) =>
Adjunction path space | path -> space, space -> path where
  leftAdjunct :: (path top -> bot) -> top -> space bot
  unit :: top -> space (path top) 
  rightAdjunct :: (top -> space bot) -> path top -> bot
  counit :: path (space bot) -> bot 
  -- minimum required impl: unit xor leftAdjunct
  -- minimum required impl: counit xor rightAdjunct
  unit = leftAdjunct id
  leftAdjunct f = fmap f . unit
  counit = rightAdjunct id
  rightAdjunct g = counit . fmap g

-- Here are some instances for different arities:

instance Adjunction ((,) a) ((->) a) where
 unit t = \arg -> (arg,t)
 counit (x,f) = f x

newtype Func2 a b c = Func2 (a -> b -> c)
   -- Func2 is only needed due to syntax of partial type constructor application

instance Adjunction ((,,) a b) (Func2 a b) where
  unit t = Func2 (\arg1 arg2 -> (arg1,arg2,t))
  counit (arg1,arg2,Func2 f) = f arg1 arg2

instance Functor ((,,) a b) where
  fmap f (x,y,z) = (x,y,f z)

instance Functor (Func2 a b) where
  fmap f (Func2 g) = Func2 (\a b -> f (g a b))

Here, 'leftAdjunct' is a generalization of curry and rightAdjunct is a
generalization of uncurry.
-- 
  Esa Pulkkinen
___
Haskell mailing list
[EMAIL PROTECTED]
http://www.haskell.org/mailman/listinfo/haskell