使用RankNTypes和TypeFamilies的非法多态或限定类型

我一直在努力移植llvm包以使用数据类型，类型族和类型nats，并试图通过引入新的Value类型来移除用于对值进行分类的两个新类型（ ConstValue和Value ）时遇到小问题用其常量进行参数化。

CallArgs只接受Value 'Variable a参数并提供一个函数来将Value 'Const a转换为Value 'Variable a 。 我想推广CallArgs来允许每个参数是'Const 'Variable或'Variable 。 这可能使用类型族以某种方式进行编码吗？ 我认为这可能是fundeps可行的。

{-# LANGUAGE DataKinds #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE TypeFamilies #-}

data Const = Const | Variable

data Value (c :: Const) (a :: *)

type family CallArgs a :: * 
type instance CallArgs (a -> b) = forall (c :: Const) . Value c a -> CallArgs b
type instance CallArgs (IO a)   = IO (Value 'Variable a)

...无法编译：

/tmp/blah.hs:10:1:
    Illegal polymorphic or qualified type:
      forall (c :: Const). Value c a
    In the type instance declaration for `CallArgs'

在以下解决方案工作（相当于遗留代码）的情况下，但要求用户施放每个常Value ：

type family CallArgs' a :: * 
type instance CallArgs' (a -> b) = Value 'Variable a -> CallArgs' b
type instance CallArgs' (IO a)   = IO (Value 'Variable a)

---

你要求的CallArgs有点像一个非确定性函数，它需要a -> b并返回Value 'Const a -> blah或Value 'Variable a -> blah 。 有时你可以用非确定性函数来翻转它; 的确，这一个有一个确定性的逆。

type family   UnCallArgs a
type instance UnCallArgs (Value c a -> b) = a -> UnCallArgs b
type instance UnCallArgs (IO 'Variable a) = IO a

现在，任何地方你都会写出类似的

foo :: CallArgs t -> LLVM t

或者类似的东西，你可以这样写：

foo :: t -> LLVM (UnCallArgs t)

当然，你可能想要选择一个比UnCallArgs更好的名字，也许是Native或者类似的东西，但是这样做需要一些我没有的领域知识。

---

会包装所有的c。 在为你的newtype AV工作？

{-# LANGUAGE DataKinds #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE TypeFamilies #-}

data CV = Const | Variable

data Value (c :: CV) (a :: *)

data AV a = AV (forall c. Value c a)

type family CallArgs a :: * 
type instance CallArgs (a -> b) = AV a -> CallArgs b
type instance CallArgs (IO a)   = IO (Value 'Variable a)

链接地址: http://www.djcxy.com/p/33337.html

上一篇: Illegal polymorphic or qualified type using RankNTypes and TypeFamilies

下一篇: Reading GHC Core