Logo Questions Linux Laravel Mysql Ubuntu Git Menu
 

Can I coerce an existentially quantified argument in a type constructor?

I have a data type whose (single) constructor contains an existentially quantified type variable:

data LogEvent = forall a . ToJSON a =>
            LogEvent { logTimestamp     :: Date
                     , logEventCategory :: Category
                     , logEventLevel    :: LogLevel
                     , logThreadId      :: ThreadId
                     , logPayload       :: a
                     }

When I wrote that type initially I hid the polymorphic payload because all I was interested in at the time was outputting to some file/stream. But now I want to do more interesting things for which I need to observe the actual type of a.

I understand from this question and other readings that existentially quantified type variables are unique upon each instantiation. However, given type is ToJSON a I can something like the following (pseudo-code):

 let x :: Result Foo = fromJSON $ toJSON (logPayload event)

It seems odd to be able to convert to and from JSON with a more precise type, although I can understand the rationale behind that.

So how can I rewrite that type to allow to extract logPayload if I know its type? I

like image 412
insitu Avatar asked Dec 15 '22 15:12

insitu


1 Answers

This is similar to the existential typeclass (anti-)pattern. This existential magic is equivalent to

data LogEvent = 
        LogEvent { logTimestamp     :: Date
                 , logEventCategory :: Category
                 , logEventLevel    :: LogLevel
                 , logThreadId      :: ThreadId
                 , logPayload       :: Aeson.Value
                 }

but this communicates more clearly what your structure represents. You should not expect anything from your existential structure that you would not expect from this.

On the other hand, if you do know logPayload's type, then you should encode that knowledge at the type level by moving the type variable out:

data LogEvent a = ...

At which point a value of type LogPayload Foo represents your knowledge of the payload's type. Then if you are so inclined you could define

data ALogEvent = forall a. ToJSON a => ALogEvent (LogEvent a)

for when you don't know it. In practice I have very rarely seen the need for both of these to exist, but maybe you have a use case for it.

If you know the type of logPayload at run-time, but cannot track the payload at compile time for some reason, perhaps you could add a Typeable a constraint to your existential so that you can cast without resorting to unsafeCoerce... in case you made a mistake you won't corrupt your whole program bizarrely.

like image 79
luqui Avatar answered May 12 '23 15:05

luqui