9

如果我有一个受有限约束的类型DataKind

{-# LANGUAGE DataKinds #-}

data K = A | B

data Ty (a :: K) = Ty { ... }

和一个存在类型，它忘记了类型中的确切选择K......但在传递的字典中记住了它。

class AK (t :: K) where k :: Ty t -> K
instance AK A where k _ = A
instance AK B where k _ = B

data ATy where ATy :: AK a => Ty a -> ATy

确实是这样ATy <-> Either (Ty A) (Ty B)，但是如果我想写其中一个证人，我需要使用unsafeCoerce

getATy :: ATy -> Either (Ty A) (Ty B)
getATy (ATy it) = case k it of
  A -> Left  (unsafeCoerce it)
  B -> Right (unsafeCoerce it)

所以一般来说这是可行的——我可以忘记使用的选择K并ATy部分记住使用getATy. 总之，这利用了我可用的尽可能多的类型信息。

但是，如果正确完成，这种类型的信息感觉好像应该是“显而易见的”。

有没有办法在不使用的情况下实现上述目标unsafeCoerce？有没有办法摆脱AK存在主义的束缚？这种技术是否可以完全基于数据类型提供的信息约束来执行？

4

1 回答 1

9

如果你想对存在类型进行运行时案例分析，你也需要一个单例表示：

{-# LANGUAGE DataKinds, GADTs, KindSignatures, ScopedTypeVariables #-}

data K = A | B

-- runtime version of K. 
data SK (k :: K) where
    SA :: SK A
    SB :: SK B

-- ScopedTypeVariables makes it easy to specify which "k" we want. 
class AK (k :: K) where
    k :: SK k 

instance AK A where k = SA
instance AK B where k = SB

data Ty (a :: K) = Ty

data ATy where
    ATy :: AK k => Ty k -> ATy

getATy :: ATy -> Either (Ty A) (Ty B)
getATy (ATy (ty :: Ty k)) = case (k :: SK k) of
    SA -> Left ty
    SB -> Right ty

这个singletons包可以在这里用来取消样板：

{-# LANGUAGE DataKinds, GADTs, TypeFamilies, TemplateHaskell, ScopedTypeVariables #-}

import Data.Singletons.TH

$(singletons [d| data K = A | B |])

data Ty (a :: K) = Ty

data ATy where
    ATy :: SingI k => Ty k -> ATy

getATy :: ATy -> Either (Ty A) (Ty B)
getATy (ATy (ty :: Ty k)) = case (sing :: Sing k) of
    SA -> Left ty
    SB -> Right ty

至于你的最后一个问题：

有没有办法摆脱存在主义中的 AK 约束？这种技术是否可以完全基于数据类型提供的信息约束来执行？

只要我们只有一个数据类型作为类型参数，信息不存在运行时，我们无法对其进行任何分析。例如，采用这种类型：

data ATy where
    ATy :: Ty k -> ATy

我们永远无法实例化kin Ty k；它必须保持多态性。

有多种方法可以提供运行时类型信息；正如我们所见，隐式传递的字典是一种选择：

data ATy where
   ATy :: AK k => Ty k -> ATy

这里AK k只是一个指向 an 的指针SK（因为AK该类只有一个方法，我们没有该类的字典，只有一个指向该方法的普通指针），构造函数中的一个额外字段。我们还可以选择使该字段显式：

data ATy where
    ATy :: SK k -> Ty k -> ATy

并且运行时表示几乎相同。

第三种选择是使用 GADT 构造函数对类型进行编码：

data ATy where
    ATyA :: Ty A -> ATy
    ATyB :: Ty B -> ATy

这个解决方案在性能方面非常好，因为没有空间开销，因为构造函数已经对类型进行了编码。这就像一个Either带有隐藏类型参数的。

于 2014-06-24T14:21:55.757 回答