从DataKinds限制的存在类型中检索信息 [英] Retrieving information from DataKinds constrained existential types

问题描述

如果我的数据类型受限于 DataKind

  { - ＃LANGUAGE DataKinds＃ - } 
 
 data K = A | B 
 
 data Ty（a :: K）= Ty {...} 
  

以及一个存在类型，它忘记了类型中的 K 的确切选择......但是可以在传入的字典中记住它。

  class AK（t :: K）其中k :: Ty t  - > K 
实例AK A其中k _ = A 
实例AK B其中k _ = B 
 
数据ATy其中ATy :: AK a =>> Ty a  - > ATy 
  

真的是这样的情况： ATy< - >或者（Ty A）（Ty B），但是如果我想写这些证人中的一个，我需要使用 unsafeCoerce

  getATy :: ATy  - > （Ty A）（Ty B）
 getATy（ATy it）= case k it of 
 A  - >离开（不安全Coerce it）
 B  - >正确（不安全Coerce it）
  

---

我可以忘记使用 ATy 来选择 K ，并使用 getATy 。总之，这充分利用了我已有的类型信息。

然而，如果正确完成，这种类型信息应该是明显的。 p>

有没有办法在不使用 unsafeCoerce 的情况下达到上述目的？有没有办法摆脱存在的 AK 约束？这种技术可以完全基于数据类型提供的信息约束吗？

在存在类型中，您还需要单例表示形式：

  { - ＃LANGUAGE DataKinds，GADTs，KindSignatures，ScopedTypeVariables＃ - } 
 
 data K = A | B 
 
  -  K.的运行时版本
数据SK（k :: K）其中
 SA :: SK A 
 SB :: SK B 
 
  -  ScopedTypeVariables可以很容易地指定我们想要的k。 
 class AK（k :: K）其中
k :: SK k 
 
实例AK A其中k = SA 
实例AK B其中k = SB 
 
 data Ty（a :: K）= Ty 
 
 data ATy其中
 ATy :: AK k => Ty k  - > ATy 
 
 getATy :: ATy  - >或者（Ty A）（Ty B）
 getATy（ATy（ty :: Ty k））= case（k :: SK k）
 SA  - >左ty 
 SB  - >正确的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  - >或者（Ty A）（Ty B）
 getATy（ATy（ty :: Ty k））= case（sing :: Sing k）
 SA  - >左ty 
 SB  - >对你最后一个问题：
 
  
 
 
 
 
 $ b  blockquote> 
 
有没有办法摆脱存在中的AK限制？ 
这种技术可以完全基于数据类型提供的信息
约束吗？
 
 
因为我们只有一种数据类型作为类型参数，所以信息不存在运行时，我们也不能对它进行任何分析。例如，采取以下类型： 
 
 
  data ATy where 
 ATy :: Ty k  - > ATy 
  
我们永远不能实例化 k  in  Ty k ;它必须保持多态。  
 
 
有多种方式可以提供运行时类型信息;隐式传递字典是一种选择，正如我们所见：
 
 
  data ATy其中
 ATy :: AK k = > Ty k  - > ATy 
  
这里 AK k 只是一个指针到 SK （因为 AK 类只有一个方法，所以我们没有该类的字典，只是一个指向该方法的普通指针），构造函数中的一个额外字段。我们也可以选择使该字段明确： 
 
 
  data ATy where 
 ATy :: SK k  - > Ty k  - > ATy 
  
和运行时表示方式几乎相同。
 
 
 
第三个选项是使用GADT构造函数来编码类型： 
 
 
  data ATy其中
 ATyA :: Ty A  - > ATy 
 ATyB :: Ty B  - > ATy 
  
这个解决方案非常好，因为没有空间开销，因为构造函数已经编码类型。它就像一个或者带有隐藏类型参数。
 
If I have a type constrained by a finite DataKind
{-# LANGUAGE DataKinds #-}

data K = A | B

data Ty (a :: K) = Ty { ... }
and an existential type which forgets the exact choice of K in the type... but remembers it in a passed dictionary.
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
it's genuinely the case that ATy <-> Either (Ty A) (Ty B), but if I want to write one of those witnesses I need to use unsafeCoerce
getATy :: ATy -> Either (Ty A) (Ty B)
getATy (ATy it) = case k it of
  A -> Left  (unsafeCoerce it)
  B -> Right (unsafeCoerce it)




So generally this works—I can forget the choice of K using ATy and remember it partially using getATy. Altogether this takes advantage of as much type information as I have available.

However, this type information feels as though it ought to be "obvious" if done correctly.

Is there a way to achieve the above without the use of unsafeCoerce? Is there a way to get rid of that AK constraint in the existential? Can this technique be performed based entirely off the information constraints provided by the data kind?
解决方案
If you want to do runtime case analysis on the existential type, you need a singleton representation too: 
{-# 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
The singletons package can be used here to do away with the boilerplate:
{-# 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
As to your last question:

  
Is there a way to get rid of that AK constraint in the existential?
  Can this technique be performed based entirely off the information
  constraints provided by the data kind?
As long as we have a data kind only as a type parameter, the information doesn't exist runtime, and we can't do any analysis on it. For example, take this type:
data ATy where
    ATy :: Ty k -> ATy
we can never instantiate the k in Ty k; it must remain polymorphic. 

There are multiple ways to provide runtime type information; implicitly passed dictionaries is one option, as we've seen:
data ATy where
   ATy :: AK k => Ty k -> ATy
Here AK k is just a pointer to an SK (since the AK class only has a single method, we don't have a dictionary for the class, just a plain pointer to the method), an extra field in the constructor. We could also choose to make that field explicit:
data ATy where
    ATy :: SK k -> Ty k -> ATy
and the runtime representation would be pretty much the same.

A third option would be using GADT constructors to encode the types:
data ATy where
    ATyA :: Ty A -> ATy
    ATyB :: Ty B -> ATy
This solution is pretty nice performance wise, since there is no space overhead, as the constructors already encode the types. It's like an Either with hidden type parameters.

                        
这篇关于从DataKinds限制的存在类型中检索信息的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！