我可以在类型构造函数中强制存在量化的参数吗？

Question

我有一个数据类型,其(单个)构造函数包含一个存在量化的类型变量:

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

当我最初编写该类型时,我隐藏了多态有效负载,因为我当时感兴趣的是输出到某个文件/流.但现在我想做更多有趣的事情,我需要观察它的实际类型a.

我从这个问题和其他读物中了解到,存在量化的类型变量在每个实例化时都是唯一的.但是,给定类型是ToJSON a我可以像下面这样(伪代码):

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

能够以更精确的类型转换为JSON和从JSON转换似乎很奇怪,尽管我可以理解其背后的基本原理.

那么logPayload如果我知道它的类型,如何重写该类型以允许提取？一世

Answer 1

这类似于存在类型(反)模式.这种存在的魔法相当于

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

但这更清楚地传达了你的结构所代表的东西.你不应该期望从你的存在结构中得到任何你不会期望的东西.

另一方面,如果您确实知道了logPayload类型,那么您应该通过移动类型变量来在类型级别编码该知识:

data LogEvent a = ...

此时,type的值LogPayload Foo表示您对有效负载类型的了解.如果你这么倾向你可以定义

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

因为当你不知道它.在实践中,我很少看到这两者都存在的必要性,但也许你有一个用例.

如果你知道logPayload运行时的类型,但由于某些原因无法在编译时跟踪有效负载,也许你可以Typeable a为你的存在主义添加一个约束,这样你就可以在不诉诸的unsafeCoerce情况下进行投射......如果你犯了一个错误你不会奇怪地破坏整个程序.