从DataKinds中检索信息约束存在类型

Question

如果我有一个受限制的类型 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存在主义中的约束？这种技术可以完全基于数据类型提供的信息约束来执行吗？

Answer 1

如果要对存在类型进行运行时案例分析,还需要单例表示:

{-# 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

我们永远不能实例化k的Ty k; 它必须保持多态.

有多种方法可以提供运行时类型信息; 隐含地通过字典是一种选择,正如我们所见:

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

这里AK k只是一个指针SK(因为AK类只有一个方法,我们没有类的字典,只是指向方法的普通指针),构造函数中有一个额外的字段.我们也可以选择明确该字段:

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

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

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

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

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