Logo Questions Linux Laravel Mysql Ubuntu Git Menu
 

polymorphic function on existential type

So say I have a class:

class C a where
  reduce :: a -> Int

Now I want to pack it up in a data type:

data Signal = forall a. (C a) => Signal [(Double, a)]

Thanks to the existential quantification, I can call C methods on Signals, but Signals don't expose a type parameter:

reduceSig :: Signal -> [(Double, Int)]
reduceSig (Signal sig) = map (second reduce) sig

Now since C has a number of methods my natural next step is to pull out the 'reduce' function so I can substitute any method:

mapsig :: (C a) => (a -> a) -> Signal -> Signal
mapsig f (Signal sig) = Signal (map (second f) sig)

Type error! Could not deduce (a1 ~ a). On further thought, I think what it's saying is that 'f' is a function on some instance of C, but I can't guarantee it's the same instance of C as in the Signals, because the type parameters are concealed! I wanted it, I got it.

So does this mean it's impossible to generalize reduceSig? I can live with this, but I'm so used to freely factoring out functions in haskell it feels strange to be obliged to write the boilerplate. On the other hand, I can't think of any way to express that a type is equal to the type inside of Signal, short of giving Signal a type parameter.

like image 985
Evan Laforge Avatar asked Dec 17 '11 05:12

Evan Laforge


People also ask

What is existential type?

Existential types, or 'existentials' for short, are a way of 'squashing' a group of types into one, single type. Existentials are part of GHC's type system extensions.

What is existential type Swift?

Existentials in Swift allow defining a dynamic value conforming to a specific protocol. Using primary associated types, we can constrain existentials to certain boundaries. The Swift team introduced the any keyword to let developers explicitly opt-in to a performance impact that might otherwise not be visible.


1 Answers

What you need to express is that f, like reduce used in reduceSig, can be applied to any type that is an instance of C, as opposed to the current type, where f works on a single type that is an instance of C. This can be done like so:

mapsig :: (forall a. (C a) => a -> a) -> Signal -> Signal
mapsig f (Signal sig) = Signal (map (second f) sig)

You'll need the RankNTypes extension, as you often do when using existential types; note that the implementation of mapsig is the same, the type has just been generalised.

Basically, with this type, mapsig gets to decide which a the function is called on; with your previous type, the caller of mapsig gets to decide that, which doesn't work, because only mapsig knows the correct a, i.e. the one inside the Signal.

However, mapsig reduce does not work, for the obvious reason that reduce :: (C a) => a -> Int, and you don't know that a is Int! You need to give mapsig a more general type (with the same implementation):

mapsig :: (C b) => (forall a. (C a) => a -> b) -> Signal -> Signal

i.e., f is a function taking any type that is an instance of C, and producing a type that is an instance of C (that type is fixed at the time of the mapsig call and chosen by the caller; i.e. while the value mapsig f can be called on any Signal, it will always produce a Signal with the same a as a result (not that you can inspect this from outside).)

Existentials and rank-N types are very tricky indeed, so this might take a bit of time to digest. :)


As an addendum, it's worth pointing out that if all the functions in C look like a -> r for some r, then you would be better off creating a record instead, i.e. turning

class C a where
  reduce :: a -> Int
  foo :: a -> (String, Double)
  bar :: a -> ByteString -> Magic

data Signal = forall a. (C a) => Signal [(Double, a)]

mapsig :: (C b) => (forall a. (C a) => a -> b) -> Signal -> Signal

into

data C = C
  { reduce :: Int
  , foo :: (String, Double)
  , bar :: ByteString -> Magic
  }

data Signal = Signal [(Double, C)]

mapsig :: (C -> C) -> Signal -> Signal

These two Signal types are actually equivalent! The benefits of the former solution only appear when you have other data types that use C without existentially quantifying it, so that you can have code that uses special knowledge and operations of the specific instance of C it's using. If your primary use-cases of this class are through existential quantification, you probably don't want it in the first place. But I don't know what your program looks like :)

like image 129
ehird Avatar answered Oct 06 '22 19:10

ehird