Can you partially restrict a type in Haskell?

Question

Is it possible to provide type signatures to Haskell values ​​that contain spaces for the type inference algorithm to populate?

An exceptionally contrived example for context:

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

It works. Using isJust m in b restricts the type m to Maybe <something> , and the definition of m limits the type m to <something> (Char, ((String, String), String, [String], String), String) , and the compiler combines these two pieces of information to determine the exact type of m .

But I’ll say that I don’t apply any Maybe special functions to m , so I need a manual type signature to stop return polymorphic. I can not say this:

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

because it is not true. Type Maybe a Not Maybe a for all a , it Maybe a for some a I would like the compiler to output; there is enough information in the program for the compiler, and in the first example we can see that the compiler is able to match several restrictions for a type, where one restriction is not enough to find out what a type is, but together they completely determine the type.

What I want is to give types of type m :: Maybe _ , where _ means "you find out what is happening here", and not "this is a hard variable of the type", as in m :: Maybe a .

Is there a way to say something like this? The alternatives that I see explicitly give the full type:

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

Or providing a type signature of the part of the expression that has the effect of restricting the Maybe part of the type signature, but not a , for example:

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

Or leave m without an explicit type signature and introduce unused additional definitions that limit m :

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

Or directly using the monomorphic function:

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

Obviously, this does not apply to Maybe , as well as to an argument to a constructor of the type * -> * ; I can imagine what I want to say: "This value is a monadic Int , for some monad" without the desire to say "this value is a monadic Int for any monad" or "this is a function from Int to some other type" without a word "is a function from Int to any other type. "

I'm more interested in whether there is something that allows me to rightly declare directly declarations like the ones above about values ​​for readability purposes, and not hard to read workarounds (like giving an explicit type signature for return ), I know that if my goal is simply to get more information about typing into the compiler to close it due to ambiguous type variables, there are countless ways to do this.

Answer 1

With GHC 7.10, there is now a PartialTypeSignatures extension that allows you to specify the hypothetical underscore syntax that I wrote in my question. Examples from the document page above:

 not' :: Bool -> _ not' x = not x -- Inferred: Bool -> Bool maybools :: _ maybools = Just [True] -- Inferred: Maybe [Bool] just1 :: _ Int just1 = Just 1 -- Inferred: Maybe Int filterInt :: _ -> _ -> [Int] filterInt = filter -- has type forall a. (a -> Bool) -> [a] -> [a] -- Inferred: (Int -> Bool) -> [Int] -> [Int] 

Only with the PartialTypeSignatures extension PartialTypeSignatures compiler generate warnings with the specified type if they were just placeholders that you intended to fill before the final version. With the addition of the -fno-warn-partial-type-signatures flag, you can say that you intended to leave the partial parts.

Answer 2

GHC does not allow you to specify partial signatures directly, unfortunately, although that would be great.

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

---

This is a good point that you make in your comment - undefined :: SomeType me 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 there are no visible results.

Answer 3

You can 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 trick in classy-prelude when providing asByteString , asSet , asList , etc.

Answer 4

Synthesizing a bit from Michael Snoyan's suggestion if I:

• I didn’t want to define a specific function for every type statement I wanted to make.
• wanted to have a type written close to what I was making a type statement about
• no need to write type twice

I could do something like:

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