The following doesn't seem to work. Is this a limitation of the current
implementation or will it never work? Are there any work arounds without introducing extra type params into the data type E? > class G a b | a -> b where > data E a :: * > wrap :: b -> E a > unwrap :: E a -> b > instance G a b where > data E a = EC b -- this line - the b is not in scope. > wrap = EC > unwrap (EC b) = b I get "Not in scope: type variable `b'". I was rather hoping it would be in scope. I've tried: > instance forall a b . G a b where > ... but that doesn't seem to extend the scope as it does with functions. I realise this is bleeding edge stuff. But I can't seem to work out from the various wiki pages on this whether this is going to be eventually supported. This is all with today's GHC HEAD. Cheers, Matthew -- Matthew Sackman http://www.wellquite.org/ _______________________________________________ Haskell-Cafe mailing list [hidden email] http://www.haskell.org/mailman/listinfo/haskell-cafe |
On Sat, May 19, 2007 at 08:40:46PM +0100, Matthew Sackman wrote:
> The following doesn't seem to work. Is this a limitation of the current > implementation or will it never work? Are there any work arounds without > introducing extra type params into the data type E? > > > class G a b | a -> b where > > data E a :: * > > wrap :: b -> E a > > unwrap :: E a -> b > > > instance G a b where > > data E a = EC b -- this line - the b is not in scope. > > wrap = EC > > unwrap (EC b) = b > > I get "Not in scope: type variable `b'". I was rather hoping it would be > in scope. Having thought about this for some time, I think I can see a reason that this might not be possible. Classes are open, thus the a -> b does not ensure that there will only ever be one E a for each unique a in G a b, given multiple modules. >From the paper [0], pg 10: "We could also in principle allow an associated type to mention only a subset of its parent class parameters; but then we would need to make extra tests to ensure the instance declarations did not overlap taking into account only the selected class parameters to ensure the type translation described by \Omega is confluent." Well, I suppose that given the open type classes, the instance declarations can overlap, despite the fundep. Does this mean that until we get closed classes, this sort of thing is impossible (without ugly workarounds)? Any thoughts at all? Anyone? Is it the case that associated types really allow nothing that can't be done with fundeps? [0] "Associated Types with Class" http://www.cse.unsw.edu.au/~chak/papers/CKPM05.html Matthew -- Matthew Sackman http://www.wellquite.org/ _______________________________________________ Haskell-Cafe mailing list [hidden email] http://www.haskell.org/mailman/listinfo/haskell-cafe |
In reply to this post by Matthew Sackman-2
| The following doesn't seem to work. Is this a limitation of the current
| implementation or will it never work? Are there any work arounds without | introducing extra type params into the data type E? | | > class G a b | a -> b where | > data E a :: * | > wrap :: b -> E a | > unwrap :: E a -> b | | > instance G a b where | > data E a = EC b -- this line - the b is not in scope. | > wrap = EC | > unwrap (EC b) = b | | I get "Not in scope: type variable `b'". That's a bug. b should be in scope However, your program is very suspicious! Associated data types *replace* functional dependencies, so you should not use both. Your probably want something like class G a where data E a :: * wrap :: a -> E a unwrap :: E a -> a Simon _______________________________________________ Haskell-Cafe mailing list [hidden email] http://www.haskell.org/mailman/listinfo/haskell-cafe |
On Mon, May 21, 2007 at 10:36:00AM +0100, Simon Peyton-Jones wrote:
> | The following doesn't seem to work. Is this a limitation of the current > | implementation or will it never work? Are there any work arounds without > | introducing extra type params into the data type E? > | > | > class G a b | a -> b where > | > data E a :: * > | > wrap :: b -> E a > | > unwrap :: E a -> b > | > | > instance G a b where > | > data E a = EC b -- this line - the b is not in scope. > | > wrap = EC > | > unwrap (EC b) = b > | > | I get "Not in scope: type variable `b'". > > That's a bug. b should be in scope Ahh, cool. I which case I wonder if this too is a bug? : data Nil = Nil data Cons :: * -> * -> * where Cons :: val -> tail -> Cons val tail class F c v t | c -> v t where data FD c t :: * instance F (Cons v t) v t where -- this blows up with "conflicting definitions for `t'" data FD (Cons v t) t = FDC v > However, your program is very suspicious! Associated data types > *replace* functional dependencies, so you should not use both. Your > probably want something like > class G a where > data E a :: * > wrap :: a -> E a > unwrap :: E a -> a I'm afraid not. I really need wrap to take a 'b' and unwrap to return a 'b'. Talking on #haskell to sjanssen last night, he came up with: class F a b where data F a :: * instance F a b where data F a = F b cast :: (F a b, F a c) => b -> c cast x = case F x of (F y) -> y as evidence as to why it's unsafe. But with the fundep, I would have thought it would have been safe. The associated type "way" would be to drop the b and then have data F a :: * -> * - just like in the papers. But I really need the b to be part of the class in order to match the b against other class constraints in other functions. In particular I need to be able to write something like: instance (G a b) => F a b where ... Somehow I doubt it, but is the following any less suspicious? class F a b where type BThing a :: * data FD a :: * wrap :: b -> FD a unwrap :: FD a -> b instance F a b where type BThing a = b data FD a = FDC (BThing a) wrap b = FDC b unwrap (FDC b) = b Incidentally, that "type BThing a = b" line also blows up with "Not in scope: type variable `b'". Thanks, Matthew -- Matthew Sackman http://www.wellquite.org/ _______________________________________________ Haskell-Cafe mailing list [hidden email] http://www.haskell.org/mailman/listinfo/haskell-cafe |
| > | > instance G a b where
| > | > data E a = EC b -- this line - the b is not in scope. | > | > wrap = EC | > | > unwrap (EC b) = b | > | | > | I get "Not in scope: type variable `b'". | > | > That's a bug. b should be in scope I was wrong. It's not a bug. E is supposed to be a type *function*, so it can't mention anything on the RHS that is not bound on the LHS. We'll improve the documentation. | Ahh, cool. I which case I wonder if this too is a bug? : | | data Nil = Nil | data Cons :: * -> * -> * where | Cons :: val -> tail -> Cons val tail | | class F c v t | c -> v t where | data FD c t :: * | | instance F (Cons v t) v t where | -- this blows up with "conflicting definitions for `t'" | data FD (Cons v t) t = FDC v As I said, associated types are an *alternative* to fundeps. We have not even begun to think about what happens if you use both of them together. You should not need to do so. | Somehow I doubt it, but is the following any less suspicious? | | class F a b where | type BThing a :: * | data FD a :: * | wrap :: b -> FD a | unwrap :: FD a -> b | | instance F a b where | type BThing a = b | data FD a = FDC (BThing a) | wrap b = FDC b | unwrap (FDC b) = b | | Incidentally, that "type BThing a = b" line also blows up with | "Not in scope: type variable `b'". No, that is wrong in the same way as before. BThing is a *function* so its results must depend only on its arguments. S _______________________________________________ Haskell-Cafe mailing list [hidden email] http://www.haskell.org/mailman/listinfo/haskell-cafe |
On Mon, May 21, 2007 at 12:39:20PM +0100, Simon Peyton-Jones wrote:
> | > | > instance G a b where > | > | > data E a = EC b -- this line - the b is not in scope. > | > | > wrap = EC > | > | > unwrap (EC b) = b > | > | > | > | I get "Not in scope: type variable `b'". > | > > | > That's a bug. b should be in scope > > I was wrong. It's not a bug. E is supposed to be a type *function*, > so it can't mention anything on the RHS that is not bound on the LHS. > We'll improve the documentation. Ok, thanks for the clarification. One final question then, how could I rewrite the following in associated types: class OneStep a b | a -> b instance OneStep (Cons v t) t class TwoStep a b | a -> b instance (OneStep a b, OneStep b c) => TwoStep a c If the fundep and b is dropped then I get: class OneStep a data OS a :: * instance OneStep (Cons v t) data OS (Cons v t) = t class TwoStep a data TS a :: * instance (OneStep a, OneStep b) => TwoStep a This last one can't be right, as I can't express the fact that the OS in "OneStep a" provides the link with "OneStep b". So is there a way to achieve this sort of chaining with associated types? Sure, the fundep version requires undecidable instances, but I've been writing quite a lot of code lately that requires that! Many thanks, Matthew -- Matthew Sackman http://www.wellquite.org/ _______________________________________________ Haskell-Cafe mailing list [hidden email] http://www.haskell.org/mailman/listinfo/haskell-cafe |
> class OneStep a
> data OS a :: * > instance OneStep (Cons v t) > data OS (Cons v t) = t > > class TwoStep a > data TS a :: * > instance (OneStep a, OneStep b) => TwoStep a instance (OneStep a, OneStep (OS a)) => TwoStep a ? Cheers, Andres _______________________________________________ Haskell-Cafe mailing list [hidden email] http://www.haskell.org/mailman/listinfo/haskell-cafe |
In reply to this post by Matthew Sackman-2
> Ok, thanks for the clarification. One final question then, how could I
> rewrite the following in associated types: > > class OneStep a b | a -> b > instance OneStep (Cons v t) t > > class TwoStep a b | a -> b > instance (OneStep a b, OneStep b c) => TwoStep a c > > If the fundep and b is dropped then I get: > > class OneStep a > data OS a :: * > instance OneStep (Cons v t) > data OS (Cons v t) = t <<<< data constructor missing !!! > > class TwoStep a > data TS a :: * > instance (OneStep a, OneStep b) => TwoStep a > > This last one can't be right, as I can't express the fact that the OS in > "OneStep a" provides the link with "OneStep b". So is there a way to > achieve this sort of chaining with associated types? You'd have to write > class OneStep a > data OS a :: * > instance OneStep (Cons v t) > data OS (Cons v t) = OSC t > > class TwoStep a > data TS a :: * > instance (OneStep a, OneStep (OS a)) => TwoStep a where > type TS a = TSC (OS (OS a)) which seems rather awkward with all these additional data type constructors. You'd be better off with associated type synonyms: > class OneStep a > type OS a :: * > instance OneStep (Cons v t) > type OS (Cons v t) = t > > class TwoStep a > type TS a :: * > instance (OneStep a, OneStep (OS a)) => TwoStep a > type TS a = OS (OS a) which are currently under development. -- Tom Schrijvers Department of Computer Science K.U. Leuven Celestijnenlaan 200A B-3001 Heverlee Belgium tel: +32 16 327544 e-mail: [hidden email] _______________________________________________ Haskell-Cafe mailing list [hidden email] http://www.haskell.org/mailman/listinfo/haskell-cafe |
In reply to this post by Andres Loeh-2
Andres Loeh <[hidden email]> wrote:
> > class OneStep a > > data OS a :: * > > instance OneStep (Cons v t) > > data OS (Cons v t) = t > > > > class TwoStep a > > data TS a :: * > > instance (OneStep a, OneStep b) => TwoStep a > > instance (OneStep a, OneStep (OS a)) => TwoStep a > ? Doesn't seem to work. Ok, my original was wrong as I had no constructor on the associated type. So below are 2 versions, one with fundeps, which works, one with associated type synonynms which doesn't work, which made me remember the warnings about how type synonynms aren't fully implemented yet, and so I wrote a third version with indexed types, but whilst I can make it work, wrapping up values in indexed types gets really really messy. > {-# OPTIONS_GHC -fglasgow-exts -fallow-undecidable-instances #-} > > module TestProb where > > data Nil = Nil > data Cons v t = Cons v t > > class OneStep a b | a -> b > instance OneStep (Cons v t) t > > class TwoStep a b | a -> b > instance (OneStep a b, OneStep b c) => TwoStep a c > > class OneStep' a where > type OS' a :: * > > instance OneStep' (Cons v t) where > type OS' (Cons v t) = t > > class TwoStep' a where > type TS' a :: * > > instance (OneStep' a, OneStep' (OS' a)) => TwoStep' a where > type TS' a = (OS' (OS' a)) > > foo :: (TwoStep a b) => a -> b -> Bool > foo _ _ = True > > foo' :: (TwoStep' a) => a -> TS' a -> Bool > foo' _ _ = True *TestProb> foo (Cons True (Cons 'b' (Cons "hello" Nil))) (Cons "boo" Nil) True *TestProb> :t foo (Cons True (Cons 'b' (Cons "hello" Nil))) foo (Cons True (Cons 'b' (Cons "hello" Nil))) :: Cons [Char] Nil -> Bool *TestProb> :t foo' (Cons True (Cons 'b' (Cons "hello" Nil))) <interactive>:1:0: No instance for (OneStep' (OS' (Cons Bool (Cons Char (Cons [Char] Nil))))) arising from a use of `foo'' at <interactive>:1:0-45 Possible fix: add an instance declaration for (OneStep' (OS' (Cons Bool (Cons Char (Cons [Char] Nil))))) Mmm. This is as a result of the instance (OneStep' a, OneStep' (OS' a)) constraint. Is it just me or does this look like the type synonynm isn't being applied? So how about adding: > instance (OneStep' a) => OneStep' (OS' a) where > type OS' (OS' a) = a *TestProb> :t foo' (Cons True (Cons 'c' (Cons 5.3 (Cons "hello" Nil)))) foo' (Cons True (Cons 'c' (Cons 5.3 (Cons "hello" Nil)))) :: (Fractional t) => TS' (Cons Bool (Cons Char (Cons t (Cons [Char] Nil)))) -> Bool Okay, but how do I inhabit that type? *TestProb> :t foo' (Cons True (Cons 'c' (Cons 5.3 (Cons "hello" Nil)))) (Cons 5.3 (Cons "hello" Nil)) <interactive>:1:59: Couldn't match expected type `TS' (Cons Bool (Cons Char (Cons t (Cons [Char] Nil))))' against inferred type `Cons t1 (Cons [Char] Nil)' In the second argument of `foo'', namely `(Cons 5.3 (Cons "hello" Nil))' So now, the third (and final!) version using indexed types: > class OneStep'' a where > data OS'' a :: * > mkOS'' :: a -> OS'' a > > instance OneStep'' (Cons v t) where > data OS'' (Cons v t) = OSC'' t > mkOS'' (Cons v t) = OSC'' t > > instance (OneStep'' a) => OneStep'' (OS'' a) where > data OS'' (OS'' a) = OSC''w a > > class TwoStep'' a where > data TS'' a :: * > mkTS'' :: a -> TS'' a > > instance (OneStep'' a, OneStep'' (OS'' a)) => TwoStep'' a where > data TS'' a = TSC'' (OS'' (OS'' a)) > mkTS'' = TSC'' . mkOS'' . mkOS'' > > foo'' :: (TwoStep'' a) => a -> TS'' a -> Bool > foo'' _ _ = True This, sort of works: *TestProb> let ts = mkTS'' (Cons True (Cons 'c' (Cons 5.3 (Cons "hello" Nil)))) in foo'' (Cons True (Cons 'c' (Cons 5.3 (Cons "hello" Nil)))) ts True But of course, the wrapping into the indexed type demands the use of mkTS''. You can't even write: *TestProb> let ts = mkOS'' (Cons 'c' (Cons 5.3 (Cons "hello" Nil))) in foo'' (Cons True (Cons 'c' (Cons 5.3 (Cons "hello" Nil)))) ts <interactive>:1:119: Couldn't match expected type `TS'' (Cons Bool (Cons Char (Cons t (Cons [Char] Nil))))' against inferred type `OS'' (Cons Char (Cons t1 (Cons [Char] Nil)))' In the second argument of `foo''', namely `ts' In the expression: let ts = mkOS'' (Cons 'c' (Cons 5.3 (Cons "hello" Nil))) in foo'' (Cons True (Cons 'c' (Cons 5.3 (Cons "hello" Nil)))) ts In the definition of `it': it = let ts = mkOS'' (Cons 'c' (Cons 5.3 (Cons "hello" Nil))) in foo'' (Cons True (Cons 'c' (Cons 5.3 (Cons "hello" Nil)))) ts Further, it is *impossible* to define mkTS'' for the extra instance "instance (OneStep'' a) => OneStep'' (OS'' a) where" as to do so would demand unwrapping the supplied (OS'' a) which can't be done - if you try to add unwrop :: OS'' a -> a to the class OneStep'' then try to define it for the Cons instance - I've thrown away v so how are you going to get it back? undefined? Matthew -- Matthew Sackman http://www.wellquite.org/ _______________________________________________ Haskell-Cafe mailing list [hidden email] http://www.haskell.org/mailman/listinfo/haskell-cafe |
On Mon, May 21, 2007 at 02:08:13PM +0100, Matthew Sackman wrote:
> Further, it is *impossible* to define mkTS'' for the extra ^^^^ -- should be mkOS'' But actually, in that code, the data declaration was never even used either - all that is needed is: instance (OneStep'' a) => OneStep'' (OS'' a) But it does rather leave a mess in the code. Matthew -- Matthew Sackman http://www.wellquite.org/ _______________________________________________ Haskell-Cafe mailing list [hidden email] http://www.haskell.org/mailman/listinfo/haskell-cafe |
In reply to this post by Matthew Sackman-2
Matthew Sackman wrote:
> > class G a where > > data E a :: * > > wrap :: a -> E a > > unwrap :: E a -> a > > I'm afraid not. I really need wrap to take a 'b' and unwrap to return a 'b'. > Talking on #haskell to sjanssen last night, he came up with: How does class F a where data B a :: * data E a :: * wrap :: B a -> E a unwrap :: E a -> B a sound? 'B a' would represent the 'b' in your previous attempt, class F a b | a -> b where ... Bertram _______________________________________________ Haskell-Cafe mailing list [hidden email] http://www.haskell.org/mailman/listinfo/haskell-cafe |
Bertram Felgenhauer:
> How does > > class F a where > data B a :: * > data E a :: * > wrap :: B a -> E a > unwrap :: E a -> B a > > sound? 'B a' would represent the 'b' in your previous attempt, > > class F a b | a -> b where > ... > I'm with Simon in thinking that this code is suspicious. For any given call to "wrap" or "unwrap", how is the compiler supposed to determine which instance to use, given that "a" cannot be uniquely determined from the type of the function? The same question also applies to Matthew's original formulation using functional dependencies: > class G a b | a -> b where > data E a :: * > wrap :: b -> E a > unwrap :: E a -> b Simon's reformulation doesn't have this problem: > class G a where > data E a :: * > wrap :: a -> E a > unwrap :: E a -> a _______________________________________________ Haskell-Cafe mailing list [hidden email] http://www.haskell.org/mailman/listinfo/haskell-cafe |
Matthew Brecknell wrote:
> Bertram Felgenhauer: > > How does > > > > class F a where > > data B a :: * > > data E a :: * > > wrap :: B a -> E a > > unwrap :: E a -> B a > > > > sound? 'B a' would represent the 'b' in your previous attempt, > > > > class F a b | a -> b where > > ... > > > > I'm with Simon in thinking that this code is suspicious. It wasn't my code Simon was replying to. > For any given call to "wrap" or "unwrap", how is the compiler supposed > to determine which instance to use, given that "a" cannot be uniquely > determined from the type of the function? As far as my limited understanding goes this should work, because we are using an associated *data* type here. This means we can't have instances saying 'type B a = Int', we have to use either a newtype or a data declaration for that. As a side effect, the compiler can determine 'a' from 'B a'. This wouldn't be possible for associated type synonyms, but those aren't completely implemented yet anyway (again, as far as I know). Bertram _______________________________________________ Haskell-Cafe mailing list [hidden email] http://www.haskell.org/mailman/listinfo/haskell-cafe |
In reply to this post by Matthew Brecknell
"Matthew Brecknell" <[hidden email]> wrote:
> Bertram Felgenhauer: > > How does > > > > class F a where > > data B a :: * > > data E a :: * > > wrap :: B a -> E a > > unwrap :: E a -> B a > > > For any given call to "wrap" or "unwrap", how is the compiler supposed > to determine which instance to use, given that "a" cannot be uniquely > determined from the type of the function? If it can't be uniquely determined then it blows up, as always. As far as my understanding of type classes goes, for any call to a function in a type class, the compiler must be able to determine a single instance to call. So if all we know is that we have a "B a" then all we can do is hope there's an instance "F a". > The same question also applies > to Matthew's original formulation using functional dependencies: > > > class G a b | a -> b where > > data E a :: * > > wrap :: b -> E a > > unwrap :: E a -> b Well here you certainly have less information, but you can still determine the instance - in both wrap and unwrap you have an "E a" which means the compiler will be able to work out some constraints on "a". There's also a "b" so it can also check that the fundep is respected, or incorporate the extra information into its decision making process. Note that both the above do type check and compile, and I have working instances of the latter: class CellBuilder c t n | c -> t n where data Cell c :: * makeCell :: t -> (MVar (Cell n)) -> Cell c unpackCell :: Cell c -> (t, (MVar (Cell n))) instance CellBuilder (Cons t n) t n where data Cell (Cons t n) = CellCons t (MVar (Cell n)) makeCell v mvar = CellCons v mvar unpackCell (CellCons v mvar) = (v, mvar) Matthew -- Matthew Sackman http://www.wellquite.org/ _______________________________________________ Haskell-Cafe mailing list [hidden email] http://www.haskell.org/mailman/listinfo/haskell-cafe |
In reply to this post by Matthew Sackman-2
Matthew Sackman wrote:
> Andres Loeh <[hidden email]> wrote: >>> class OneStep a >>> data OS a :: * >>> instance OneStep (Cons v t) >>> data OS (Cons v t) = t >>> >>> class TwoStep a >>> data TS a :: * >>> instance (OneStep a, OneStep b) => TwoStep a >> instance (OneStep a, OneStep (OS a)) => TwoStep a >> ? > > Doesn't seem to work. Ok, my original was wrong as I had no constructor > on the associated type. So below are 2 versions, one with fundeps, which > works, one with associated type synonynms which doesn't work, which > made me remember the warnings about how type synonynms aren't fully > implemented yet, and so I wrote a third version with indexed types, but > whilst I can make it work, wrapping up values in indexed types gets > really really messy. Yes, it's messy with indexed data families as they force you to introduce all these new constructors and the corresponding wrapping and unwrapping code. As Tom wrote in another message in this thread, you really do want to use indexed synonyms families (aka associated type synonyms) here. They will do what you want. We are currently working on completing the implementation of synonym families.[1] Manuel [1] For those who wonder why this is taking so long, we are working on a system that is actually significantly more general than what we described in the ICFP05 paper. In particular, we want synonym families to play nice with GADTs. _______________________________________________ Haskell-Cafe mailing list [hidden email] http://www.haskell.org/mailman/listinfo/haskell-cafe |
Free forum by Nabble | Edit this page |