Logo Questions Linux Laravel Mysql Ubuntu Git Menu
 

Type signature for function with possibly polymorphic arguments

Tags:

haskell

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)
like image 213
Clinton Avatar asked Jul 27 '16 03:07

Clinton


2 Answers

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 f2 into a context expecting a function of type, say, Int -> [Int], GHC will apply f2 to the necessary type for you (i.e., instantiate f2 to a specific type), and all will be well. For example, if you have

g :: (Int -> [Int]) -> Bool

and you apply g to f, GHC will actually compile that to

g (f @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.

like image 172
dfeuer Avatar answered Oct 05 '22 03:10

dfeuer


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).

like image 35
David Young Avatar answered Oct 05 '22 03:10

David Young