Re: Equality constraints (~): type-theory behind them
er that. (Superclass constraints took up to >> > about 2010.) >> > >> > Suppose I wanted just the (~) parts of those implementations. Which >> > would be the best place to look? (The Users Guide doesn't give a >> > reference.) ICFP 2008 'Type Checking with Open Type Functions' shows >> > uses of (~) in user-written code, but doesn't explain it or motivate it >> > as a separate feature. >> > >> > My specific question is: long before (~), it was possible to write a >> > TypeCast class, with bidirectional FunDeps to improve each type >> > parameter from the other. But for the compiler to see the type >> > improvement at term level, typically you also need a typeCast method and >> > to explicitly wrap a term in it. If you just wrote a term of type `a` in >> > a place where `b` was wanted, the compiler would either fail to see your >> > `TypeCast a b`, or unify the two too eagerly, then infer an overall type >> > that wasn't general enough. >> > >> > (For that reason, the instance for TypeCast goes through some >> > devious/indirect other classes/instances or exploits separate >> > compilation, to hide what's going on from the compiler's enthusiasm.) >> > >> > But (~) does some sort of magic: it's a kinda typeclass but without a >> > method. How does it mesh with type improvement in the goldilocks zone: >> > neither too eager nor too lazy? >> > >> > >> > AntC >> >> >> ___ > Glasgow-haskell-users mailing list > Glasgow-haskell-users@haskell.org > http://mail.haskell.org/cgi-bin/mailman/listinfo/glasgow-haskell-users > -- prof. dr. ir. Tom Schrijvers Research Professor KU Leuven Department of Computer Science Celestijnenlaan 200A 3001 Leuven Belgium Phone: +32 16 327 830 http://people.cs.kuleuven.be/~tom.schrijvers/ ___ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.org http://mail.haskell.org/cgi-bin/mailman/listinfo/glasgow-haskell-users
Re: Does this, and should this type check on GHC 6.10.x ?
We got a code (please refer to the attached lhs file) that uses type families and type classes very cleverly. We don't know who wrote itbecause this was a contribution of an anonymous reviewer on our paper, which we are still revising. http://kyagrd.dyndns.org/wiki/SharedSubtypes Although we learned a lot from this code, we still have unsolved question about this code. The problem is, we are still not sure whether this code actually type checks in any GHC version, and we are not even sure whether this should type check or not as it is. Have you first, before you turn to GHC< considered whether this code should be well-typed in any type system? Review3.lhs:67:29: Could not deduce (Expandable (Tuple (Map ((,) t2) ys))) from the context (xs ~ t2 ::: ts2, Expandable t2) arising from a use of `:::' at Review3.lhs:67:29-59 At first sight, it looks like this constraint Expandable (Tuple (Map ((,) t2) ys)) is indeed one that's required to hold in order to make the code well-typed. Do you agree? Yet I see no instance of Expandable for Tuple. So why do you think this constraint should hold anyway? Tom -- Tom Schrijvers Department of Computer Science K.U. Leuven Celestijnenlaan 200A B-3001 Heverlee Belgium tel: +32 16 327544 e-mail: tom.schrijv...@cs.kuleuven.be url: http://www.cs.kuleuven.be/~toms/ Disclaimer: http://www.kuleuven.be/cwis/email_disclaimer.htm ___ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
Re: Type checker loops with type families, overlapping and undecidable instances
-- Uncommenting the line below causes the typechecker to loop (GHC 6.10.1, Windows) --test = f Zero Is this expected behavior or a bug? The call f Zero requires a co-inductive proof of the type class constraint (F Nat): F Nat <=> Vieweable Nat /\ F' (View Nat) <=> True /\ F' (Unit :+: Nat) <=> True /\ F Unit /\ F Nat <=> True /\ True /\ F Nat The type checker does have functionality for such co-inductive proof (generating co-inductive dictionaries), but apparently it's not kicking in here. Probably because of the separate fixedpoint loops for type classes and type families in the checker. -- Tom Schrijvers Department of Computer Science K.U. Leuven Celestijnenlaan 200A B-3001 Heverlee Belgium tel: +32 16 327544 e-mail: [EMAIL PROTECTED] url: http://www.cs.kuleuven.be/~toms/ ___ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
RE: flexible contexts and context reduction
On Thu, 27 Mar 2008, Sittampalam, Ganesh wrote:
Well, Ord Foo doesn't hold, does it? So Ord (a, b) isn't equivalent to
(Ord a, Ord b).
It seems you (can) throw logic out of the window with flexible instances.
So there's no point in talking about equivalences any more. We could still
capture the operational aspect of it, but we'd need the type/data family
counterpart of flexible instances.
Considering overlapping instances, there is still a logic, but it's
implicit in the notation. You'd get for your
example:
(a /= Foo \/ b \= Foo) ==> (Ord a /\ Ord b <=> Ord (a,b))
Again, an overlapping type/data family would be needed for encoding this
in dictionaries.
Cheers,
Tom
-Original Message-
From: Simon Peyton-Jones [mailto:[EMAIL PROTECTED]
Sent: 27 March 2008 09:05
To: Sittampalam, Ganesh; 'Tom Schrijvers'; Ganesh Sittampalam
Cc: glasgow-haskell-users@haskell.org; Martin Sulzmann
Subject: RE: flexible contexts and context reduction
Why "unfortunately"? Looks fine to me.
Simon
|
| Unfortunately, GHC accepts the following:
|
| {-# LANGUAGE FlexibleInstances #-}
| module Foo2 where
|
| data Foo = Foo
| deriving Eq
|
| instance Ord (Foo, Foo) where
| (Foo, Foo) < (Foo, Foo) = False
==
Please access the attached hyperlink for an important electronic communications
disclaimer:
http://www.credit-suisse.com/legal/en/disclaimer_email_ib.html
==
___
Glasgow-haskell-users mailing list
Glasgow-haskell-users@haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
--
Tom Schrijvers
Department of Computer Science
K.U. Leuven
Celestijnenlaan 200A
B-3001 Heverlee
Belgium
tel: +32 16 327544
e-mail: [EMAIL PROTECTED]
url: http://www.cs.kuleuven.be/~toms/
___
Glasgow-haskell-users mailing list
Glasgow-haskell-users@haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
RE: flexible contexts and context reduction
You're talking about something else: the dictionaries (Ord a, Ord b) from which the Ord
(a,b) dictionary were constructed. We don't have a very good name for these guys, but
"superclass" isn't a good one.
Otherwise I agree with all you say. Your idea of using type families is cool.
| data OrdDict a =
| { (<) :: a -> a -> Bool
| , ...
| , super :: Super a
| }
|
| type family Super a :: *
| type instance Super Int = ()
| type instance Super [a] = OrdDict a
| type instance Super (a,b) = (OrdDict a, OrdDict b)
|
| A similar solution is possible with a data family Super (but obviously I'm
| in favor of type families :)
Can you say why? A data family would work fine here. But it's not a big deal.
Just a matter of taste, and familiarity.
So the other question is whether this is useful. How often do people write
stuff like this?
f :: Ord [a] => a -> a -> Bool
f x y = x>y
This paper has some examples, I believe:
Modular Generic Programming with Extensible Superclasses
Martin Sulzmann and Meng Wang
In Workshop on Generic Programming (WGP'06)
http://www.comp.nus.edu.sg/~sulzmann/publications/wgp06-modulargeneric.ps
Nevertheless, I hadn't realised it was possible before, and now I can see it is.
I'd be nice to know of people who need or would like to have this feature.
Tom
--
Tom Schrijvers
Department of Computer Science
K.U. Leuven
Celestijnenlaan 200A
B-3001 Heverlee
Belgium
tel: +32 16 327544
e-mail: [EMAIL PROTECTED]
url: http://www.cs.kuleuven.be/~toms/
___
Glasgow-haskell-users mailing list
Glasgow-haskell-users@haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
Re: flexible contexts and context reduction
On Wed, 26 Mar 2008, Ganesh Sittampalam wrote:
On Wed, 26 Mar 2008, Ross Paterson wrote:
On Wed, Mar 26, 2008 at 08:52:43PM +, Ganesh Sittampalam wrote:
I'm a bit confused about why the following program doesn't compile (in
any of 6.6.1, 6.8.1 and 6.9.20080316). Shouldn't the Ord (a, b) context
be reduced?
To use bar, you need (Ord a, Ord b). You're assuming that Ord (a, b)
implies that, but it's the other way round.
Logically, the implication holds. There's an equivalence:
Ord a /\ Ord b <=> Ord (a,b)
Why it does or doesn't work in a Haskell impelmentation iss an
implementation issue / language design issue.. There's a paper by Martin
Sulzmann about extensible superclasses, which shows how this can be
implemented if you don't use dictionaries for your typeclasses, but the
type-passing scheme.
The problem with dictionaries is that you have to store the superclass
dictionaries, here Ord a and Ord b, in the dictionary, here Ord (a,b).
However, what superclass dictionaries you have to store depends on the
instance, e.g. Ord Int doesn't have any superclass and Ord [a] has
superclass Ord a.
There maybe wasn't an easy solution, but here is my idea of how to
to it with data or type families. The dictionary type would be:
data OrdDict a =
{ (<) :: a -> a -> Bool
, ...
, super :: Super a
}
type family Super a :: *
type instance Super Int = ()
type instance Super [a] = OrdDict a
type instance Super (a,b) = (OrdDict a, OrdDict b)
A similar solution is possible with a data family Super (but obviously I'm
in favor of type families :) The openness of the family matches the
openness of the type classes.
There is a little overhead in carrying around the superclasses.
Now ask your favorite Haskell system to implement this feature :)
Tom
--
Tom Schrijvers
Department of Computer Science
K.U. Leuven
Celestijnenlaan 200A
B-3001 Heverlee
Belgium
tel: +32 16 327544
e-mail: [EMAIL PROTECTED]
url: http://www.cs.kuleuven.be/~toms/
___
Glasgow-haskell-users mailing list
Glasgow-haskell-users@haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
Re: type families + GADT = type unsafety?
(Simon, does this mean that non-~ discharging will become subject to GADT-style type annotation rules?) No, it does not. No type annotations required in non-GADT-related code, even if equalities are involved. Tom -- Tom Schrijvers Department of Computer Science K.U. Leuven Celestijnenlaan 200A B-3001 Heverlee Belgium tel: +32 16 327544 e-mail: [EMAIL PROTECTED] ___ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
