11

我一直在缓慢地移植llvm包以使用数据类型、类型族和类型 nats，并在尝试通过引入由其参数化的新类型来删除用于对值（ConstValue和）进行分类的两种新类型时遇到了一个小问题恒常性。ValueValue

CallArgs仅接受Value 'Variable a参数并提供将 a 转换为 a 的Value 'Const a函数Value 'Variable a。我想概括CallArgs一下，允许每个参数是'Constor '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)。价值约
    在“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)
4

2 回答 2

6

CallArgs你要求的有点像一个非确定性函数，它接受并a -> b返回Value 'Const a -> blahor 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、maybeNative或类似名称更好的名称，但要做到这一点需要一些我没有的领域知识。

于 2012-12-12T20:23:31.880 回答
3

将包装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)
于 2012-12-12T21:06:59.180 回答