我可以在類型構造函數中強制存在量化參數嗎？

Question

我有一個數據類型，其（單）構造包含一個存在性量化類型變量：

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

當我寫那種最初我躲在多態有效載荷，因爲所有我感興趣的是在當時被輸出到一些文件/流。但現在我想做更多有趣的事情，我需要觀察a的實際類型。

我明白從this question和其他讀數，存在量化類型變量在每個實例化是唯一的。然而，由於類型爲ToJSON a我可以像下面這樣（僞代碼）：

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

這似乎很奇怪是能夠轉換和從JSON用更精確的類型，但我能理解背後的基本原理那。

那麼，如果我知道它的類型，我該如何重寫該類型以允許提取logPayload？我

Answer 1

這與existential typeclass（反模式）類似。這種存在的魔法相當於

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

但這更清楚地表明你的結構代表什麼。你不應該期望從你的存在結構中得到任何你不會期望的東西。

在另一方面，如果你做知道logPayload的類型，那麼你應該編碼的知識在類型級別通過移動類型變量出來：

data LogEvent a = ... 

在該點的值鍵入LogPayload Foo代表您對有效負載類型的瞭解。那麼如果你這麼傾向於你可以定義

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

當你不知道它。在實踐中，我很少看到這兩種存在的必要性，但也許你有一個用例。

如果你知道logPayload在運行時的類型，但不能跟蹤在編譯時的有效載荷出於某種原因，也許你可以一個Typeable a約束添加到您的存在，這樣就可以不訴諸unsafeCoerce投...如果你犯了一個錯誤，你不會奇怪地破壞你的整個程序。

Answer 2

那麼如果我知道它的類型，我該如何重寫該類型以允許提取logPayload？

如果你不想改變你的類型，你可以替換fromJSON & toJSON通過unsafeCoerce - 同樣的想法，如果你是對的，但如果你不正確有關的類型可能會崩潰您的程序相同的結果。

如果您想讓類型檢查器確保您是正確的，那麼必須在LogEvent中公開類型a，而不要使用存在類型。

Answer 3

你可能會考慮給Data.Typeable一個鏡頭;將Typeable a約束放入您的存在類型中，然後如果您可以正確猜出隱藏類型，則可以將該值返回到該類型下。玩具示例見this Gist。

請注意，這種技術會犧牲一些類型安全性 - 如果您開始在LogEvent之內放入其他類型的內容，您可能會破壞假定它們成功處理每個子內容的類型的用戶。與代數類型不同，動態和強制類型意味着編譯器無法幫助您證明詳盡性。