RE: fundeps for extended Monad definition
> The reason, which is thoroughly explained in Simon Peyton-Jones' > message, is that the given type signature is wrong: it should read > f1 :: (exists b. (C Int b) => Int -> b) Sigh, read this after posting :) ___ Haskell mailing list [EMAIL PROTECTED] http://www.haskell.org/mailman/listinfo/haskell
Re: fundeps known beforehand (was RE: fundeps for extended Monad definition)
> Suppose we are in case 1. Then the programmer has written a too-general
> type signature on f. The programmer *must* know that b=Int in this case
> otherwise his function definition makes no sense. However, I don't really
> see a reason why this should be an error rather than just a warning. If
> some other module K imports both U and (for instance) I2, then we'll get a
> fundep clash and the whole program will be invalid.
I now retract this comment :). Clearly this is just as bad as saying:
> f :: Bool -> b
> f x = x
since this claims that it will take a Bool and produce a value of type b
for all types b. However, would it be all right to say (in
pseudo-Haskell):
> f :: exists b . Bool -> b
> f x = x
?
Here, we're simply claiming that there is *some* type b for which f takes
a Bool and produces a b?
I believe this same analysis extends to something like:
> class C a b | a -> b where {}
> instance C Int Int where {}
> f :: exists b . C Int b => Int -> b
> f i = i
It seems that this would be legal in a language like haskell but which
allowed existensial quantification.
Am I correct?
___
Haskell mailing list
[EMAIL PROTECTED]
http://www.haskell.org/mailman/listinfo/haskell
RE: fundeps for extended Monad definition
Hello!
Simon Peyton-Jones wrote:
> class C a b | a -> b where {}
> instance C Int Int where {}
> f1 :: (forall b. (C Int b) => Int -> b)
> f1 x = undefined
Indeed, this gives an error message
Cannot unify the type-signature variable `b' with the type `Int'
Expected type: Int
Inferred type: b
The reason, which is thoroughly explained in Simon Peyton-Jones'
message, is that the given type signature is wrong: it should read
f1 :: (exists b. (C Int b) => Int -> b)
Alas, 'exists' is not an allowed type quantifier. Not explicitly that
is. We can get 'exists' if we use the permitted 'forall' in a negative
position (aka in an existential type).
The following code
> class C a b | a -> b where {}
> instance C Int Int where {}
> newtype M a = M (forall b.(C a b) => b)
> f :: Int -> M Int
> f x = M undefined
typechecks in both Haskell compilers.
Hal Daume's original example works as well:
> newtype MM2 m a = MM2 (forall mb.(Monad2 m a mb) => mb)
> class Monad2 m a ma | m a -> ma, ma -> m a where
> return2 :: a -> ma
> bind2 :: ma -> (a -> (MM2 m a)) -> (MM2 m a)
> unused :: m a -> ()
> unused = \_ -> ()
> instance Monad2 [] a [a] where
>bind2 = error "urk"
Again, it typechecks both in Hugs and GHC.
___
Haskell mailing list
[EMAIL PROTECTED]
http://www.haskell.org/mailman/listinfo/haskell
Announce: Haskell Data Clustering
Hi all, I've had some software which implements a variety of unsupervised learning (aka clustering) algorithms around for some time, but finally got around to making the source code available. I thought some people on this list might find it of interest, so I include a pointer which explains how it is used: http://www.isi.edu/~hdaume/GDC/ Happy clustering! - Hal -- Hal Daume III | [EMAIL PROTECTED] "Arrest this man, he talks in maths." | www.isi.edu/~hdaume ___ Haskell mailing list [EMAIL PROTECTED] http://www.haskell.org/mailman/listinfo/haskell
Re: Re : escape from existential quantification
> It occasionally happens that I *know* what type is (or at least ought to be) inside > an existential type, but unfortunately GHC doesn't, and I need to get the value out. > This can be solved using dynamic types, for example you declare the datatype as You can also use an unsafe cast operation if you know statically what the type will be, but the compiler doesn't. See for example http://www.isi.edu/~hdaume/haskell/NewBinary/TestBits.hs for an example of this. It essentially has a function which writes items of arbitrary type (in a list) to a binary memory location and then reads the back. When reading them back, the only way to know the type is to look at the type of the corresponding item on the "write" list. It relies on this to make the casting really a safe operation. ___ Haskell mailing list [EMAIL PROTECTED] http://www.haskell.org/mailman/listinfo/haskell
Re : escape from existential quantification
Wang Meng wrote I understand that existentially bound types cannot escape. For example, say we have data Foo = forall a. Foo Int a Then we cannot define a function extract (Foo i a) = a However,this limitation makes it extremly difficult to program with local quantifications.Is there any way to by pass this? It occasionally happens that I *know* what type is (or at least ought to be) inside an existential type, but unfortunately GHC doesn't, and I need to get the value out. This can be solved using dynamic types, for example you declare the datatype as > data Foo = forall a. Typeable a => Foo Int a (or something like that), then you can extract the a value by going to Dynamic and back. ___ Haskell mailing list [EMAIL PROTECTED] http://www.haskell.org/mailman/listinfo/haskell
Re: escape from existential quantification
On Thu, 27 Feb 2003 18:26:31 + Keith Wansbrough <[EMAIL PROTECTED]> wrote: > > The idea is to use a type more like this: > > data Foo = forall a. Foo Int a (a -> (Int,Bool)) (a -> Int) (a -> > Foo) > > where the functions are the operations you want to use on the data Or else one can use type classes: - data Foo = forall a. Show a => Foo a instance Show Foo where show (Foo x) = show x main = print [Foo 3,Foo "ciao"] - Vincenzo -- Mai pensato a cosa vuol dire 10 anni di embargo? Si può chiedere ad una popolazione ormai allo stremo di subire un'altra guerra e magari un secondo embargo? Cosa c'entrano i bambini che muoiono di fame, di radiazioni e di mancanza di medicine con i giochi di potere di un dittatore? Che colpa ne portano? Leggere per esempio: http://www.fulviopoglio.com/salvi1.htm ___ Haskell mailing list [EMAIL PROTECTED] http://www.haskell.org/mailman/listinfo/haskell
Re: escape from existential quantification
> I understand that existentially bound types cannot escape. > > For example, say we have > data Foo = forall a. Foo Int a > > Then we cannot define a function > extract (Foo i a) = a > > However,this limitation makes it extremly difficult to program with local > quantifications.Is there any way to by pass this? The idea is to use a type more like this: data Foo = forall a. Foo Int a (a -> (Int,Bool)) (a -> Int) (a -> Foo) where the functions are the operations you want to use on the data. So now a list of Foos can contain data of many different types, as long as it is paired with the appropriate accessor functions for those types. You can use it like this: case x of Foo n x f g h -> if snd (f x) then g x else 0 for example. --KW 8-) -- Keith Wansbrough <[EMAIL PROTECTED]> http://www.cl.cam.ac.uk/users/kw217/ University of Cambridge Computer Laboratory. ___ Haskell mailing list [EMAIL PROTECTED] http://www.haskell.org/mailman/listinfo/haskell
fundeps known beforehand (was RE: fundeps for extended Monad definition)
Hi Simon, all,
> Here's a less complicated variant of the same problem:
>
> class C a b | a -> b where {}
>
> instance C Int Int where {}
>
> f :: (C Int b) => Int -> b
> f x = x
This is interesting, but I'm not entirely sure what the problem is (from a
theoretical, not practical, standpoint). Obviously there is no problem in
a one module program, so let's assume we have the following modules:
module C where
class C a b | a -> b where {}
module I1 where
import C
instance C Int Int where {}
module I2 where
import C
instance C Int Bool where {}
module U where
import C
import ?
f :: C Int b => Int -> b
f x = x
Now, there are four cases:
1) U (transitively) imports I1
2) U (transitively) imports I2
3) U (transitively) imports both I1 and I2
4) U (transitively) imports neither I1 nor I2
Suppose we are in case 1. Then the programmer has written a too-general
type signature on f. The programmer *must* know that b=Int in this case
otherwise his function definition makes no sense. However, I don't really
see a reason why this should be an error rather than just a warning. If
some other module K imports both U and (for instance) I2, then we'll get a
fundep clash and the whole program will be invalid.
Suppose we are in case 2. Then the programmer has clearly screwed up
because we know b=Bool and x::Int and x::Bool are incompatible. This
should clearly be a type error.
Case 3 is impossible, as this will be a fundep clash.
Case 4 should produce an error (IMO). Of course, there could be a module
K which imports this U and also I1 in which case you might argue that this
should be allowed, but I don't think that makes much sense.
> I suppose I could use (unsafeCoerce x) as the RHS, which amounts to
> saying "in every call to f, b will be Int, so we know that the coercion
> is safe". But that is a scarily global property. For example, if a
> call site of f does not "see" the instance declaration, it might call f
> with an argument of type (C Int Bool) or something. Nor can I see an
> easy way to insert the 'right' coercions in general.
Is this possible? In order for this to happen, this evil module M must
import U. This means that it has transitively imported I1 and thus has
the instance declaration. Or am I missing something. I think the
unsafeCoerce x is safe in these cases.
> Bottom line: excellent point, but I can't see how to fix it. Maybe
> there are some fundep experts out there who can guide us through the
> swamp?
Yes, please!
- Hal
___
Haskell mailing list
[EMAIL PROTECTED]
http://www.haskell.org/mailman/listinfo/haskell
escape from existential quantification
I understand that existentially bound types cannot escape. For example, say we have data Foo = forall a. Foo Int a Then we cannot define a function extract (Foo i a) = a However,this limitation makes it extremly difficult to program with local quantifications.Is there any way to by pass this? -W-M- @ @ | \_/ ___ Haskell mailing list [EMAIL PROTECTED] http://www.haskell.org/mailman/listinfo/haskell
RE: fundeps for extended Monad definition
Interesting example
| class Monad2 m a ma | m a -> ma, ma -> m a where
| return2 :: a -> ma
| bind2 :: Monad2 m b mb => ma -> (a -> mb) -> mb
| _unused :: m a -> ()
| _unused = \_ -> ()
| instance Monad2 [] a [a] where
| bind2 = error "urk"
The functional dependencies say
m a -> ma
Instantiating this with the instance declaration
instance Monad2 [] a [a]
we can deduce that
given any constraint (Monad2 t1 t2 t3),
if t1 = [], then t3 must be [t2]
In the instance declaration, we instantiate the type of bind2 to get
the type of bind2 needed for this particular instance declaration:
bind2 :: forall b mb. Monad2 [] b mb => ma -> (a -> mb) -> mb
Now the rule above says "that means mb must be [b]" and that gives rise
to the error.
GHC is consistent about this --- if you don't supply an defn for bind2,
it makes one up, and complains in more or less the same way.
Here's a less complicated variant of the same problem:
class C a b | a -> b where {}
instance C Int Int where {}
f :: (C Int b) => Int -> b
f x = x
Is the defn of f legal? Both GHC and Hugs reject it because the
inferred type of f is more like
C Int Int => Int -> Int
Functional dependencies tell us that 'b' must be Int, so in fact the two
types are equivalent. In this example the programmer could write the
'correct' type, but in your case you can't because the type signature
arises by instantiating the one in the class declaration.
I'm really not sure what to do about this. GHC has an excellent way of
keeping me honest in type-checking: the type checker has to produce a
translation of the program into the (typed) core language. What could
f's translation look like. It must presumably be
f (d::C Int Int) (x::Int) = x
giving f the type
f :: C Int Int -> Int -> Int
Another translation could be
f b (d::C Int b) (x::Int) = x
(the 'b' is a type variable, a big-lambda binding) giving f the type
f :: forall b. C Int b -> Int -> Int
But what I *cannot* get is the type
f : forall b. C Int b -> Int -> b
how could I write the term?
f b (d:: C Int b) (x::Int) = ?
I suppose I could use (unsafeCoerce x) as the RHS, which amounts to
saying "in every call to f, b will be Int, so we know that the coercion
is safe". But that is a scarily global property. For example, if a
call site of f does not "see" the instance declaration, it might call f
with an argument of type (C Int Bool) or something. Nor can I see an
easy way to insert the 'right' coercions in general.
Bottom line: excellent point, but I can't see how to fix it. Maybe
there are some fundep experts out there who can guide us through the
swamp?
Simon
___
Haskell mailing list
[EMAIL PROTECTED]
http://www.haskell.org/mailman/listinfo/haskell
