受限制的封闭式家庭 [英] Constrained closed type family

查看：104
本文介绍了受限制的封闭式家庭的处理方法，对大家解决问题具有一定的参考价值，需要的朋友们下面随着小编来一起学习吧！

问题描述

我能说服编译器，一个封闭类型系列中的类型同义词总是满足一个约束吗？这个家庭被一系列有价值的促销价值索引。



数据NoShow = NoShow
数据LiftedType = V1 | V2 | V3

type family（Show（Synonym（a :: LiftedType））=>同义词（a :: LiftedType）其中
同义词V1 = Int
同义词V2 = NoShow - no Show instance =>编译错误
同义词V3 =（）

我可以在开放类型族上强制执行一个约束： 

  class（Show（Synonym a））=> SynonymClass（a :: LiftedType）其中
类型同义词a 
类型同义词a =（）
 
实例同义词类Int其中
类型同义词V1 = Int 
 
  - 编译器在此抱怨
实例SynonymClass V2其中
类型同义词V2 = NoShow 
 
实例SynonymClass V3

，但是编译器必须能够推断出存在 SynonymClass a V1 ， V2 和 V3 中的每一个，但是无论如何，我宁愿不使用开放式的系列。



我要求这个的动机是我想说服编译器，我的代码中的封闭类型系列具有Show / Read实例。一个简单的例子是：

  parseLTandSynonym :: LiftedType  - >字符串 - > String 
 parseLTandSynonym lt x = 
 case（toSing lt）of 
 SomeSing（slt :: SLiftedType lt'） - > parseSynonym slt x 
 
 parseSynonym :: forall lt。 SLiftedType lt  - >字符串 - >字符串
 parseSynonym slt flv = 
 case（readEither flv :: Either String（Synonym lt））of 
 Left err  - > Can not parse synonym：++ err 
 Right x  - > 同义词的值：++ show x

[有人在评论中提到这是不可能的 - 是这是因为它在技术上是不可能的（如果是这样，为什么）或者仅仅是GHC实现的限制？]解决方案

问题是我们不能在实例头中放置 Synonym ，因为它是一个类型族，并且我们不能写出通用量化约束，如（ forall x。Show（Synonym x））=> ... 因为Haskell中没有这样的事情。然而，我们可以使用两件事：




  • > forall x。 f x - >一个相当于（存在x。f x） - >一个


  • singletons 的去功能化让我们可以将类型族放入实例头部。



因此，我们定义了一个适用于 singletons -style类型的存在封装函数：

  data Some ::（TyFun k *  - > *） - > *其中
 Some :: Sing x  - > f @@ x  - >一些f

我们还包含了 LiftedType
$ p $ import Data.Singletons.TH
import Text.Read
import Control.Applicative

$（singletons [d | data LiftedType = V1 | V2 | V3 derived（Eq，Show）|]）

type family同义词t其中
同义词V1 = Int
同义词V2 =（）
同义词V3 = Char

data同义词S :: TyFun LiftedType * - > * - 同义词
类型实例的符号应用同义词S t =同义词t

现在，我们可以使用某些同义词S->>一个而不是 forall x。同义词x - >一个，这个表单也可以用在实例中。

  instance Show（Some SynonymS）where 
 show（Some SV1 x）= show x 
 show（Some SV2 x）= show x 
 show（Some SV3 x）= show x 
 
 instance Read（一些同义词）其中
 readPrec = undefined  - 我现在不打扰... 
 
 parseLTandSynonym :: LiftedType  - >字符串 - > String 
 parseLTandSynonym lt x = 
 case（toSing lt）of 
 SomeSing（slt :: SLiftedType lt'） - > parseSynonym slt x 
 
 parseSynonym :: forall lt。 SLiftedType lt  - >字符串 - > 
 parseSynonym slt flv = 
 case（readEither flv :: Either String（Some SynonymS））of 
 Left err  - > Can not parse synonym：++ err 
 Right x  - > 同义词的值：++ show x

这并不直接为我们提供阅读（同义词t），对于 t 的任何特定选择，虽然我们仍然可以阅读某些同义词S ，然后在存在标签上进行模式匹配，以检查我们是否获得了正确的类型（如果不正确，则失败）。这几乎涵盖了 read 的所有用例。



如果这还不够好，我们可以使用另一个包装器，并将一些f 实例提升为普遍量化的实例。 

 数据At ::（TyFun k *  - > *） - > k  - > *其中
 At :: Sing x  - > f @@ x  - >在fx

在fx 相当于 f @@ x ，但我们可以为它编写实例。特别是，我们可以在这里写出一个明智的通用 Read 实例。 

 实例（Read（某些f），SDecide（KindOf x），SingKind（KindOf x），SingI x）=> 
 Read（At fx）其中
 readPrec = do 
某些标签x < -  readPrec :: ReadPrec（某些f）
大小写标签％〜（唱歌：唱歌x） 
 Proved Refl  - >纯（标签x）
反驳_  - >空

我们首先解析一些f ，然后检查解析的类型索引是否等于我们想要解析的索引。这是我上面提到的用于解析具有特定索引的类型的抽象。这更方便，因为我们在 At 的模式匹配中只有一个例子，无论我们有多少个索引。注意通过 SDecide 约束。它提供了％〜方法，如果我们包含派生方程式， singletons 在单例数据定义中。使用这个：

  parseSynonym :: forall lt。 SLiftedType lt  - >字符串 - > String 
 parseSynonym slt flv = withSingI slt $ 
 case（readEither flv :: Either String（At SynonymS lt））of 
 Left err  - > Can not parse synonym：++ err 
 Right（At tag x） - > 同义词的值：++ show（Some tag x :: Some SynonymS）

我们也可以制作 At 和一些之间的转换更容易一点：

  curry'::（forall x。At fx  - > a） - >一些f  - > a 
 curry'f（Some tag x）= f（At tag x）
 
 uncurry'::（Some f  - > a） - >在f x  - > a 
 uncurry'f（At tag x）= f（Some tag x）
 
 parseSynonym :: forall lt。 SLiftedType lt  - >字符串 - > String 
 parseSynonym slt flv = withSingI slt $ 
 case（readEither flv :: Either String（At SynonymS lt））of 
 Left err  - > Can not parse synonym：++ err 
 Right atx  - > 同义词值：++ uncurryshow atx


Can I convince the compiler that a constraint is always satisfied by the type synonyms in a closed type family? The family is indexed by a finite set of promoted values.

Something along the lines of

data NoShow = NoShow
data LiftedType = V1 | V2 | V3

type family (Show (Synonym (a :: LiftedType)) => Synonym (a :: LiftedType)) where
  Synonym V1 = Int
  Synonym V2 = NoShow -- no Show instance => compilation error
  Synonym V3 = ()

I can enforce a constraint on open type families:

class (Show (Synonym a)) => SynonymClass (a :: LiftedType) where
  type Synonym a
  type Synonym a = ()

instance SynonymClass Int where
  type Synonym V1 = Int

-- the compiler complains here
instance SynonymClass V2 where
  type Synonym V2 = NoShow

instance SynonymClass V3

but the compiler would then have to be able to reason about the fact that there exists an instance of SynonymClass a for each of V1, V2 and V3? But in any case, I'd prefer not to use an open type family.

My motivation for requiring this is that I want to convince the compiler that all instances of a closed type family in my code have Show/Read instances. A simplified example is:

parseLTandSynonym :: LiftedType -> String -> String
parseLTandSynonym lt x =
  case (toSing lt) of
    SomeSing (slt :: SLiftedType lt') -> parseSynonym slt x

parseSynonym :: forall lt. SLiftedType lt -> String -> String
parseSynonym slt flv =
      case (readEither flv :: Either String (Synonym lt)) of
        Left err -> "Can't parse synonym: " ++ err
        Right x  -> "Synonym value: " ++ show x

[Someone mentioned in the comments that it's not possible - is this because it's technically impossible (and if so, why) or just a limitation of the GHC implementation?]

解决方案

The problem is that we can't put Synonym in an instance head because it's a type family, and we can't write a "universally quantified" constraint like (forall x. Show (Synonym x)) => ... because there's no such thing in Haskell.

However, we can use two things:

  • forall x. f x -> a is equivalent to (exists x. f x) -> a
  • singletons's defunctionalization lets us put type families into instance heads anyway.

So, we define an existential wrapper that works on singletons-style type functions:

data Some :: (TyFun k * -> *) -> * where
  Some :: Sing x -> f @@ x -> Some f

And we also include the defunctionalization symbol for LiftedType:

import Data.Singletons.TH
import Text.Read
import Control.Applicative

$(singletons [d| data LiftedType = V1 | V2 | V3 deriving (Eq, Show) |])

type family Synonym t where
  Synonym V1 = Int
  Synonym V2 = ()
  Synonym V3 = Char

data SynonymS :: TyFun LiftedType * -> * -- the symbol for Synonym
type instance Apply SynonymS t = Synonym t

Now, we can use Some SynonymS -> a instead of forall x. Synonym x -> a, and this form can be also used in instances.

instance Show (Some SynonymS) where
  show (Some SV1 x) = show x
  show (Some SV2 x) = show x
  show (Some SV3 x) = show x

instance Read (Some SynonymS) where
  readPrec = undefined -- I don't bother with this now...

parseLTandSynonym :: LiftedType -> String -> String
parseLTandSynonym lt x =
  case (toSing lt) of
    SomeSing (slt :: SLiftedType lt') -> parseSynonym slt x

parseSynonym :: forall lt. SLiftedType lt -> String -> String
parseSynonym slt flv =
      case (readEither flv :: Either String (Some SynonymS)) of
        Left err -> "Can't parse synonym: " ++ err
        Right x  -> "Synonym value: " ++ show x

This doesn't directly provide us Read (Synonym t) for any specific choice of t, although we can still read Some SynonymS and then pattern match on the existential tag to check if we got the right type (and fail if it's not right). This pretty much covers all the use cases of read.

If that's not good enough, we can use another wrapper, and lift Some f instances to "universally quantified" instances. 

data At :: (TyFun k * -> *) -> k -> * where
  At :: Sing x -> f @@ x -> At f x

At f x is equivalent to f @@ x, but we can write instances for it. In particular, we can write a sensible universal Read instance here.

instance (Read (Some f), SDecide (KindOf x), SingKind (KindOf x), SingI x) =>
  Read (At f x) where
    readPrec = do
      Some tag x <- readPrec :: ReadPrec (Some f)
      case tag %~ (sing :: Sing x) of
        Proved Refl -> pure (At tag x)
        Disproved _ -> empty

We first parse a Some f, then check whether the parsed type index is equal to the index we'd like to parse. It's an abstraction of the pattern I mentioned above for parsing types with specific indices. It's more convenient because we only have a single case in the pattern match on At, no matter how many indices we have. Notice though the SDecide constraint. It provides the %~ method, and singletons derives it for us if we include deriving Eq in the singleton data definitions. Putting this to use:

parseSynonym :: forall lt. SLiftedType lt -> String -> String
parseSynonym slt flv = withSingI slt $ 
      case (readEither flv :: Either String (At SynonymS lt)) of
        Left err -> "Can't parse synonym: " ++ err
        Right (At tag x)  -> "Synonym value: " ++ show (Some tag x :: Some SynonymS)

We can also make the conversion between At and Some a bit easier:

curry' :: (forall x. At f x -> a) -> Some f -> a
curry' f (Some tag x) = f (At tag x)

uncurry' :: (Some f -> a) -> At f x -> a
uncurry' f (At tag x) = f (Some tag x)

parseSynonym :: forall lt. SLiftedType lt -> String -> String
parseSynonym slt flv = withSingI slt $ 
      case (readEither flv :: Either String (At SynonymS lt)) of
        Left err -> "Can't parse synonym: " ++ err
        Right atx  -> "Synonym value: " ++ uncurry' show atx

这篇关于受限制的封闭式家庭的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！

查看全文
相关文章
其他开发最新文章
热门教程
热门工具
登录 关闭
扫码关注1秒登录
发送“验证码”获取 | 15天全站免登陆