Can you partially constrain a type in Haskell?

Question

Is it possible to provide type signatures to Haskell values that contain "blanks" for the type inference algorithm to fill in?

Extremely contrived example for context:

m = return ('I', (("don't", "really"), "care", ["what", "this"], "type"), "is") 

b = isJust m

This works. The use of isJust m in b constrains the type of m to be Maybe <something>, and m's definition constrains the type of m to be <something> (Char, ((String, String), String, [String], String), String), and the compiler puts together those two pieces of information to work out the precise type of m.

But say I'm not applying any Maybe specific functions to m, so I'll need a manual type signature to stop the return being polymorphic. I can't say this:

m :: Maybe a
m = return ('I', (("don't", "really"), "care", ["what", "this"], "type"), "is")

because that's incorrect. The type isn't Maybe a for all a, it's Maybe a for some a I would like the compiler to infer; there is enough information in the program for the compiler to do this, and we can see from my first example that the compiler is able to put together multiple constraints on the type, where no constraint alone is sufficient to figure out what the type is but together they fully specify the type.

What I want is to be able to give types like m :: Maybe _, where the _ means "you figure out what goes here", rather than "this is a rigid type variable" as in m :: Maybe a.

Is there some way of saying something like this? The alternatives I can see are explicitly giving the full type:

m :: Maybe (Char, ((String, String), String, [String], String), String)
m = return ('I', (("don't", "really"), "care", ["what", "this"], "type"), "is")

Or giving a type signature to a part of the expression which has the effect of constraining the Maybe part of the type signature but not the a, like:

m = (return :: a -> Maybe a) ('I', (("don't", "really"), "care", ["what", "this"], "type"), "is")

Or leaving m without an explicit type signature and introducing unused extra definitions which constrain m:

m = return ('I', (("don't", "really"), "care", ["what", "this"], "type"), "is") 

b = isJust m

Or using a monomorphic function directly:

m = Just ('I', (("don't", "really"), "care", ["what", "this"], "type"), "is")

Obviously this isn't specific to Maybe, nor to the argument of a * -> * type constructor; I can imagine wanting to say "this value is a monadic Int, for some monad" without wanting to say "this value is a monadic Int for any monad", or "this is a function from Int to some other type" without saying "this is a function from Int to any other type`.

I'm mostly interested in whether there is something that allows me to fairly directly state declarations like the above about values, for readability purposes, rather than difficult to read workarounds (like giving an explicit type signature for the return). I'm aware that if my goal is to simply to get extra typing information into the compiler to shut it up about ambiguous type variables there are innumerable ways to do that.

Answer 1

GHC doesn't let you specify partial signatures directly, unfortunately, though that would be great to have.

One way to do what you want in this case is m = return ... `asTypeOf` (undefined :: Maybe a), where asTypeOf is a Prelude function :: a -> a -> a that returns its first argument but forces it to unify with the second.

---

That's a good point you make in your comment -- undefined :: SomeType makes me sad too. Here's another solution:

import Data.Proxy

proxiedAs :: a -> Proxy a -> a
proxiedAs = const

Now you can say m = return ... `proxiedAs` (Proxy :: Proxy (Maybe a)), and no ⊥s in sight.

Answer 2

You could write something like:

asMaybe :: Maybe a -> Maybe a
asMaybe = id

m = asMaybe $ return ('I', (("don't", "really"), "care", ["what", "this"], "type"), "is")

I use this kind of trick in classy-prelude, in providing asByteString, asSet, asList, etc.