将特定类型归纳为GADT中的某个类 [英] Generalizing from a specific type to a class in a GADT

问题描述

我有以下定义

{-# LANGUAGE GADTs, TypeInType, RankNTypes #-}
import Data.Kind

class Character (a :: * -> *) where
  showVal :: a b -> b -> String

data ExampleCharacter a where
  Variable :: ExampleCharacter String
  EqualSign :: ExampleCharacter ()
  Deref :: ExampleCharacter ()

instance Character ExampleCharacter where
  showVal Variable = id
  showVal EqualSign = const "="
  showVal Deref = const "*"

data Symbol :: forall a. ExampleCharacter a -> * where
  Terminal :: a -> Symbol (b :: ExampleCharacter a)

如您所见，

我定义了一个在类型签名中使用ExampleCharacters的Symbol类.用法示例为let sym = Terminal "xyy" :: Symbol Variable创建名称为"xyy"的变量符号.

as you can see I have defined a Symbol class that uses ExampleCharacters in the type signature. Example usage would be let sym = Terminal "xyy" :: Symbol Variable creating a variable symbol with the name "xyy".

现在，显而易见的下一步是将ExampleCharacter概括为Character c.我尝试了以下方法:

Now, the obvious next step would be to generalize ExampleCharacter to Character c. I tried the following:

data Symbol :: (forall c (a :: *). Character c) => c a -> * where
  Terminal :: a -> Symbol (b :: c a)

但是出现以下错误:

main.hs:22:20: error:
    • Illegal constraint in a type: forall (c :: * -> *) a. Character c
    • In the type ‘Symbol (b :: c a)’
      In the definition of data constructor ‘Terminal’
      In the data declaration for ‘Symbol’

我不太确定错误要告诉我什么.为什么forall (c :: * -> *) a. Character c是非法约束，如何成为非法约束?有什么办法解决吗?

I'm not quite sure what the error wants to tell me. Why is forall (c :: * -> *) a. Character c an illegal constraint and how so? Is there any way around it?

推荐答案

来自

由于种类和类型相同，所以种类现在可以(使用-XTypeInType) 包含类型约束. 目前仅平等约束 .我们希望这会扩展到以下方面的其他限制条件: 未来.

As kinds and types are the same, kinds can now (with -XTypeInType) contain type constraints. Only equality constraints are currently supported, however. We expect this to extend to other constraints in the future.

所以原则上您写的是明智的；它根本不被支持(在撰写本文时，最新的GHC是8.2.2).

So in principle what you've written is sensible; it simply isn't supported yet (as of writing, most recent GHC is 8.2.2).

这篇关于将特定类型归纳为GADT中的某个类的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！