[Haskell-cafe] ambiguous constraint errors

[Evan Laforge]

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