'Type signature for function with possibly polymorphic arguments
Can I, and if so, how do I, write the type signature for a function:
g f x y = (f x, f y)
Such that given:
f1 :: a -> [a]
f1 x = [x]
x1 :: Int
x1 = 42
c1 :: Char
c1 = 'c'
f2 :: Int -> Int
f2 x = 3 * x
x2 :: Int
x2 = 5
Such that:
g f1 x1 c1 == ([42], ['c']) :: ([Int], [Char])
g f2 x1 x2 == (126, 15) :: (Int, Int)
Solution 1:[1]
No, you can't. The basic problem is that Haskell's syntax has fooled you into thinking that f1
's and f2
's types are more similar than they really are. Once translated into GHC Core, they look rather more different:
f1 :: forall a . a -> [a]
f2 :: Int -> Int
Not only this, but the corresponding terms look rather different:
f1 = ?a -> ?(x :: a) -> [x]
f2 = ?(x :: Int) -> 3 * x
As you can see, f1
and f2
actually have different numbers of arguments, where f1
takes a type and a value, and f2
takes just a value.
In more usual circumstances, when you plop f1
into a context expecting a function of type, say, Int -> [Int]
, GHC will apply f1
to the necessary type for you (i.e., instantiate f1
to a specific type), and all will be well. For example, if you have
g :: (Int -> [Int]) -> Bool
and you apply g
to f1
, GHC will actually compile that to
g (f1 @Int)
But here you want polymorphism over whether that instantiation happens or not, which GHC doesn't support (I think it would be a rather radical and destructive change to the core language).
Since class instances, type family patterns, and type family results cannot be quantified, I'm pretty confident there is no way whatsoever to get what you want.
Solution 2:[2]
This is actually possible, if you don't mind adding a Proxy
argument, using a variation on my answer to a similar question here.
Most of my explanation from that answer holds here, but we need to expand on it slightly by adding a couple more helper type classes (what I'm calling List
and Both
here):
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE ConstraintKinds #-}
import Data.Proxy
f1 :: a -> [a]
f1 x = [x]
x1 :: Int
x1 = 42
c1 :: Char
c1 = 'c'
f2 :: Int -> Int
f2 x = 3 * x
x2 :: Int
x2 = 5
class b ~ [a] => List a b
instance List a [a]
class (a ~ b, b ~ c) => Both a b c
instance Both a a a
g :: (c a r1, c b r2) =>
Proxy c -> (forall x r. c x r => x -> r) -> a -> b -> (r1, r2)
g _ f x y = (f x, f y)
This allows us to do
ghci> g (Proxy :: Proxy List) f1 x1 c1
([42],"c")
ghci> g (Proxy :: Proxy (Both Int)) f2 x1 x2
(126,15)
List
and Both
are not the best names (especially List
), so you might want to come up with better ones if you do use this (although I'm not sure I would suggest doing this sort of type trickery in production code anyway, unless you have a really good reason).
Sources
This article follows the attribution requirements of Stack Overflow and is licensed under CC BY-SA 3.0.
Source: Stack Overflow
Solution | Source |
---|---|
Solution 1 | Will Ness |
Solution 2 | Community |