>> get_int sym = fmap ambi_int (lookup sym ambi_table :: Maybe (Ambi Maybe)) > > Of you and the type system you're the only one who knows that that value is > not used. The type system doesn't use (all) the rules you have in your mind. > It follows more simple ones. > > You judge by values, not only types here. That is, you look at the value of > ambi_int and see that it's just 10 in your (value again) some_ambi. You see > that it's not > > ambi_int = (some_return_from_monad ambi_monad) * 3
I'm not totally understanding, but I think you're saying that I could write ambi_int in a way that it still had type "Ambi m -> Int" but depended on the type of 'm'. I guess that makes sense, because it could "run" m internally and return an Int based on the result, which therefore depends on the type of 'm'. > Also compare with this > > x :: Int > x = "Five" > > main = putStrLn "Hello" > > This program doesn't use x, so the type error would definitely not bother us > at run-time. But it's nevertheless not ignored. Sure, my intuition has much less trouble with that one. It's off topic, but I wonder if there's lazy equivalent for type checkers. I.e. at the value level I could call it 'undefined' which works with any type (since all types include _|_ I guess), and as long as it's not evaluated, there's no problem at runtime. A type level equivalent could have a "type bottom" which represents a type checking failure, but it only affects the results of type functions if they "demand" it. I guess a more appealing direction is to try to make the value system total, not make the type system partial :) And it might destroy separate compilation. >> I've been told this doesn't mean what I expect it to, which is that >> the context constraints propagate up to and unify with the containing >> type (out of curiosity, since it's accepted, what *does* this do? I >> think I read it somewhere once, but now I forget and can't find it). >> And sure enough, using this type doesn't make my type declarations >> have the right contexts. > > Well it means that you can't call any data constructor of this type with > arguments not satisfying those constraints. Effectively it means that you > won't ever have a value of type (Command some m) in your program where the > pair (some,m) doesn't satisfy them. > > However, the type system won't leverage that fact. And when you use a value > of type Command some m somewhere you have to repeat the constraints. > > afaik it is officially considered a Haskell mis-feature. Interesting. Are there any valid uses for data context? If not, is it slated for removal? > Maybe something like > > class MyAlias t1 t2 ... > > instance (Monad some, Monad m, ...) => MyAlias some m ... I see, so sort of like using classes as "class aliases" which can reduce the amount of junk in the context. I think I've seen that convention in use before. [ isaac dupree ] > with {-# LANGUAGE GADTs #-} you should be able to use a different syntax for > the same sort of thing but with the meaning you wanted: (beware of layout > messed up by e-mail line wrapping) : > data Command some m where > Command :: (Monad some, Monad m) => some (State.StateT () m Status) -> > Command some m Interesting, I'll have to try that out. > It's a really annoying problem! The multi-param-type-class hack Daniil > Elovkov mentioned is another way it's done sometimes, that also uses a few > compiler extensions. CPP macros are even uglier but they can work too. I guess I'll just type them out explicitly, and add "automatic context propagation" to my ghc wishlist, along with records and srcloc_annotate, and other random stuff. I'm not even sure what such a feature would look like, or if it would be feasible though... Thanks for the pointers! _______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe