使用RankNTypes和TypeFamilies的非法多态或限定类型 [英] Illegal polymorphic or qualified type using RankNTypes and TypeFamilies

问题描述

我一直在努力移植 llvm 软件包以使用数据类型，类型族和类型名称，并且遇到试图通过引入一个新的 ConstValue 和 Value 来移除用于分类值的两个新类型时， code> Value 类型由其常量参数化。

CallArgs 只接受 Value'变量a 参数并提供了一个将值'Const a 转换为值'变量a 。我想概括一下 CallArgs 来允许每个参数都是'Const 或'变量。这可能使用类型族以某种方式进行编码吗？

  { - ＃LANGUAGE DataKinds＃ - } 
 { - ＃LANGUAGE RankNTypes＃ - } 
 { - ＃LANGUAGE TypeFamilies＃ - } 
 
 data Const = Const |变量
 
数据值（c :: Const）（a :: *）
 
类型系列CallArgs a :: * 
类型实例CallArgs（a  - > b）= forall（c :: Const）。值c a  - > CallArgs b 
类型实例CallArgs（IO a）= IO（Value'Variable a）
  

...无法编译：

 
 /tmp/blah.hs:10:1：
非法多态或限定类型：
 forall（c :: Const）。价值ca 
在`CallArgs'的类型实例声明中
 

在以下解决方案工作的情况下（相当于遗留代码），但需要用户输入每个常量值：

  type family CallArgs'a :: * 
类型实例CallArgs'（a  - > b）=值'变量a  - > CallArgs'b 
类型实例CallArgs'（IO a）= IO（Value'Variable a）
  

CallArgs 有点像一个非确定性函数，它需要 a - > b 并返回值'Const a - > blah 或值'变量a - >等等。有时你可以用非确定性函数来翻转它;

 类型系列UnCallArgs a 
类型实例UnCallArgs（Value ca  - > b）= a  - > UnCallArgs b 
类型实例UnCallArgs（IO'变量a）= IO a 
  

你可能写过类似于

  foo :: CallArgs t  - > LLVM t 
  

或类似的东西，您可以改为：

  foo :: t  - > LLVM（UnCallArgs t）
  

当然，您可能希望选择比<$ c $更好的名称c> UnCallArgs ，也许 Native 或类似的东西，但这样做需要一些我没有的领域知识。 p>

I've been slowly working on porting the llvm package to use data kinds, type families and type-nats and ran into a minor issue when trying to remove the two newtypes used for classifying values (ConstValue and Value) by introducing a new Value type parameterized by its constness.

CallArgs only accepts Value 'Variable a arguments and provides a function for casting a Value 'Const a to a Value 'Variable a. I'd like to generalize CallArgs to allow each argument to be either 'Const or 'Variable. Is this possible to encode this somehow using type families? I think it's probably doable with 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)

... which fails to compile:

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

Where the following solution works (equivalent to the legacy code), but requires the user to cast the each constant Value:

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

解决方案

The CallArgs you're asking for is kind of like a non-deterministic function which takes a -> b and returns either Value 'Const a -> blah or Value 'Variable a -> blah. One thing you can sometimes to with nondeterministic functions is flip them around; indeed, this one has a deterministic inverse.

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

Now, anywhere you would have written a type like

foo :: CallArgs t -> LLVM t

or something like that, you can write this instead:

foo :: t -> LLVM (UnCallArgs t)

Of course, you might want to pick a better name than UnCallArgs, maybe Native or something like that, but doing that well requires a bit of domain knowledge that I don't have.

这篇关于使用RankNTypes和TypeFamilies的非法多态或限定类型的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！