Блог

Мой код не компилируется:

 {-# 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 with implicit forall вызывает у вас горе. Самое время упомянуть анти-шаблон «экзистенциальная количественная оценка с помощью класса типов»

Поскольку вы включили ограничение 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 in конструкторы for PointSet не могут быть объединены с a in TestFunc , поскольку a in PointSet является некоторым конкретным экземпляром RealFrac , но TestFunc является функцией, которая требуется для работы для any 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' = ...