相关疑难解决方法(0)

正如问题的标题所示,我想知道什么是Levity多态性及其动机是什么？我知道这个页面里面有一些细节,但大部分的解释都是我的头脑.:)

虽然这个页面更友好,但我仍然无法理解它背后的动机.

在 Haskell 中，有时为了性能人们会使用unsafeCoerce（或更安全的coerce）在具有相同内部表示的类型之间进行转换。我所知道的最常见的例子是新类型列表：

newtype Identity a = Identity a

f :: [Identity a] -> [a]
f = coerce

现在，我在我正在处理的代码库中有两个 GADT，看起来像这样精简：

data Typ where
    PredT :: Typ
    ProcT :: [Typ] -> Typ
    IntT :: Typ
    ListT :: Typ -> Typ


data HKTyp v (f :: * -> * -> *) where
    HKPredT :: HKTyp v f
    HKProcT :: [HKTyp v f] -> HKTyp v f
    HKIntT :: HKTyp v f
    HKListT :: f v (HKTyp v f) …