haskell - GHC 无法用 GADT 和存在类型推导出 (a1 ~ a)

Question

我的代码无法编译:

{-# LANGUAGE EmptyDataDecls, GADTs, RankNTypes  #-}

import Data.Ratio

data Ellipsoid
data Halfplane

data PointSet a where
    Halfplane :: RealFrac a => a -> a -> a -> (a -> a -> Bool) -> a -> PointSet Halfplane
    Ellipsoid :: RealFrac a => a -> a -> a -> (a -> a -> Bool) -> a -> PointSet Ellipsoid

type TestFunc =  RealFrac a => (a -> a -> a ->  Bool)

ellipsoid :: PointSet Ellipsoid -> TestFunc
ellipsoid (Ellipsoid a b c f r) = f' where f' z y x = ((x/a)^2 + (y/b)^2 + (z/c)^2) `f` r

halfplane :: PointSet Halfplane -> TestFunc
halfplane (Halfplane a b c f t) = f' where f' z y x = (a*x + b*y + c*z) `f` t

我得到的错误是:

Could not deduce (a1 ~ a)
[...]
Expected type: a -> a -> a -> Bool
  Actual type: a1 -> a1 -> a1 -> Bool
In the expression: f'
[...]

对于ellipsoid和halfplane这两个函数。

我不明白并且正在寻找答案，为什么a不能与a1等同，两者都是RealFrac，甚至更好:为什么推导出两种不同的类型(a ~ a1)？

Answer 1

您对GADT的使用隐式 forall使你悲伤。现在是提一下“类型类的存在量化”的好时机 anti-pattern

由于您已包含约束 RealFrac a在 PointSet 的定义中您隐式使用 forall像这样:

data PointSet a where
    Halfplane :: forall a. RealFrac a => a -> a -> a -> (a -> a -> Bool) -> a -> PointSet HalfPlane
    Ellipsoid :: forall a. RealFrac a => ...

这同样适用于TestFunc :

type TestFunc = forall a. RealFrac a => a -> a -> a -> Bool

这就是为什么 GHC 强制您添加 RankNTypes扩展名。

因为forall a在 PointSet 的构造函数中不可能与 a 统一在TestFunc自 a在PointSet是RealFrac的一些特定实例，但是TestFunc是适用于任何 a 所需的函数。

具体类型之间的区别a和普遍量化的forall a. a导致 GHC 推断出两种不同的类型 a和a1 .

解决方案？抛弃所有这些存在主义的废话。在需要的何处和何时应用类型类约束:

{-# LANGUAGE DataKinds, GADTs, KindSignatures #-}

data Shape = Halfplane | Ellipsoid -- promoted via DataKinds

data PointSet (s :: Shape) a where
    Halfplane :: a -> a -> a -> (a -> a -> Bool) -> a -> PointSet Halfplane a
    Ellipsoid :: ...

type TestFunc a = a -> a -> a -> Bool

ellipsoid :: RealFrac a => PointSet Ellipsoid a -> TestFunc a
ellipsoid (Ellipsoid a b c f r) = f' where f' = ...

现在PointSet需要 2 个参数:幻像类型 s :: Shape其中有种类Shape (种类是类型的类型)和 a这与您的原始示例相同，除了作为 PointSet 的显式参数它不再隐含地存在量化。

为了解决您的最后一点，a和a1错误消息中不是“都是 RealFrac 。RealFrac 不是类型，它是类型类。a 和 a1 是两种潜在不同类型，两者恰好是RealFrac 的实例。

也就是说，除非您使用更具表现力的类型 PointSet有一个更简单的解决方案。

data PointSet a
    = Halfplane a a a (a -> a -> Bool) a
    | Ellipsoid a a a (a -> a -> Bool) a

testFunc :: RealFrac a => PointSet a -> TestFunc a
testFunc (Ellipsoid a b c f r) = f' where f' = ...
testFunc (Halfplane a b c f t) = f' where f' = ...