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

Question

我一直在慢慢地将llvm包移植到使用数据类型,类型族和type-nats,并在尝试删除用于分类值的两个新类型(ConstValue和Value)时通过引入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:
    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)

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或者类似的东西,但这样做很好,需要一些我没有的领域知识.