3

我不断地欺骗自己认为有可能以某种方式（至少模仿）拥有一个类型类，比如说，不受base任意约束

（对于我所有的搜索，我都没有找到任何令人满意的解决来自外部库的约束类型参数的东西）。

TL;DR我如何编写Arrow实例，即使我需要更改MyArr，但必须保留Typeable其值？：

data MyArr a b where
  Arr :: (Typeable a, Typeable b) => (a -> b) -> MyArr a b

instance Arrow MyArr where ???

考虑Arrows 的这个定义：

class Arrow p where
  arr :: (a -> b) -> p a b

有时我真的希望它是

class Arrow p where
  arr :: (Typeable a, Typeable b) => ...

我想为我上面提到的 GADT 提供它；我的构造函数带有其参数的证明Typeable：

data MyArr a b where
  Arr :: (Typeable a, Typeable b) => (a -> b) -> MyArr a b

我不能直接为此写一个Arrow实例，因为arrmust beforall a b.并且不能一般地召唤Typeable a. 我认为这是问题的症结所在。

如果我可以编写自己的，我可以使用一个善良的家庭来class Arrow使它工作：ConstraintKinds

class Arrow p where
  type ArrowC p :: * -> Constraint
  arr :: (ArrowC p a, ArrowC p b) => ...

但是由于我想保持与proc符号和其他库的兼容性，所以我不能这样做。所以我一直在想我可以以某种方式定义我的 Arrow 的数据类型，利用ConstraintKinds, or 约束, or, reify andreflection

data MyArr a b where
  Arr :: Dict (Typeable a) -> Dict (Typeable b) -> (a -> b) -> MyArr a b

但是我Dict可以将什么传递给实例的定义arr？也许

data MyArr (k :: * -> Constraint) a b where
  Arr :: (k a, k b) => (a -> b) -> MyArr k a b

但是 dangit，这也不起作用，因为arr'sa and b必须是不受约束的

我尝试过让singleton值携带证明或约束a and b的 技巧TypeFamilies，但可惜无济于事。

这些选项之一必须是可能的，对吧？

几个月来，我一直在困惑中扭曲自己，不断地重新审视这个问题，并欺骗自己认为这是可能的。

4

0 回答 0