我的代码无法编译:
{-# 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
)?
最佳答案
您对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' = ...
关于haskell - GHC 无法用 GADT 和存在类型推导出 (a1 ~ a),我们在Stack Overflow上找到一个类似的问题: https://stackoverflow.com/questions/24395644/