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

Question

我一直在慢慢地移植llvm 包以使用数据类型、类型族和类型nats，并在尝试删除用于分类值的两种新类型（ConstValue 和@ 987654324@) 通过引入一个新的Value 类型，该类型由其常量参数化。

CallArgs 只接受Value 'Variable a 参数，并提供将Value 'Const a 转换为Value 'Variable a 的函数。我想概括CallArgs 以允许每个参数为'Const 或'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: 非法多态或限定类型： forall (c :: Const)。值 c a 在“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)

Answer 1

您要求的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 或类似名称更好的名称，但要做到这一点需要一些我没有的领域知识。

Answer 2

将包装 forall 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)