递归函数依赖关系无法工作

Question

我试图在幻影类型中将单元数组(来自dimensional)相乘，并且在函数依赖方面遇到了困难。该问题的简化版本如下：

我有以下类型

data F (a:: [*]) = F String

其中，字符串以外语表示表达式，而幻影类型表示类型的列表。

我可以这样做

x = F "x" :: F '[Double]
y = F "(1,3)" :: F '[Int, Int]

我通过创建一个Nums类来实现像这样的算术运算符，这个类是一个Num列表。

class Nums (a::[*])
instance Nums '[]
instance (Num a, Nums as) => Num (a ': as)

然后我可以实例化Num F

instance Nums as => F as where
   (F a) * (F b) = F (a ++ "*" ++ b)
   ... etc ...

现在，我试着用物理单位来做同样的事情。我可以用这样的一种方式来做

import qualified Numeric.Units.Dimensional as Dim

data F (a::[*]) = F String
(!*!) :: (Num n, Dim.Mul a b c) => F '[Dim.Dimensional v a n]
                                -> F '[Dim.Dimensional v b n]
                                -> F '[Dim.Dimensional v c n]

(F a) !*! (F b) = F (a ++ "*" ++ b)

这似乎是可行的，我可以“乘以”2‘F的不同单位，结果是在科雷特单位。很明显，我想把这个推广到任何列表，并使用与Nums，我称为Muls一样的技巧。

class Muls a b c | a b -> c
instance '[] '[] '[]
instance (Num n, Mul a b c, Muls as bs cs) 
   => Muls (Dim.Dimensional v a n ': as)
           (Dim.Dimensional v b n ': bs)
           (Dim.Dimensional v c n ': cs)

!*! :: (Muls as bs cs) => F as -> F bs -> F cs
(F a) !*! (F b) = F (a ++ "*" ++ b)

我收到了一个Illegal Instance declaration错误：

Illegal instance declaration for
 ‘Muls
    (Dim.Dimensional v a n : as)
    (Dim.Dimensional v b n : bs)
    (Dim.Dimensional v c n : cs)’
 The coverage condition fails in class ‘Muls’
   for functional dependency: ‘a b -> c’
 Reason: lhs types ‘Dim.Dimensional v a n : as’, ‘Dim.Dimensional
                                                    v b n
                                                    : bs’
   do not jointly determine rhs type ‘Dim.Dimensional v c n : cs’
 Using UndecidableInstances might help
In the instance declaration for
 ‘Muls (Dim.Dimensional v a n : as) (Dim.Dimensional v b n
                                    : bs) (Dim.Dimensional v c n : cs)’

如果我使用UndecidableInstances扩展，它似乎确实有效。我的问题是，为什么我需要这个扩展，有什么办法可以避免它吗？

或者，我可能可以使用dimensional的类型家族版本来完成这个任务。不幸的是，我需要自定义单元，还不清楚dimensional-tf是否支持用户定义的单元。

Answer 1

默认情况下，Haskell要求实例选择是可判定的，也就是说，试图确定类型是否满足约束不能导致编译器中的无限循环。考虑以下代码：

class A (a :: *)
class B (a :: *) 
instance A a => B a 

显然，这个实例可能导致无限循环(它不一定会这样做！)即使其他每个实例本身都不能导致无限循环，添加这个实例也可以。在某个地方可能有严格的证据，但我不知道。

UndecidableInstances所做的唯一的事情就是说：“我保证我不会用导致无限循环的类型调用我的函数，所以即使我的实例可以产生无限循环，我也承担确保这种情况不会发生的责任。”

另一方面，表格的实例：

instance (C1 a1, C2 a2 ... Cn an) => C (T a1 a2 .. an)

不会产生无限循环，因为Haskell不允许无限类型，而且这个实例解压缩了一个构造函数，所以即使Ci引用C，最终也会得到一个具有0类型参数的类型构造函数。

如果您编写了一个不可判定的实例，则应该

test.hs:26:10:
    Constraint is no smaller than the instance head
      in the constraint: A a
    (Use UndecidableInstances to permit this)
    In the instance declaration for `B a'

我认为这是在您的情况下应该看到的错误，显示您实际看到的错误应该被认为是一个错误。