从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？有没有办法摆脱存在的约束？这种技术是否可以完全基于数据类型提供的信息约束来执行？

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。