класс типов с функцией ограниченных параметров - PullRequest
0 голосов
/ 23 сентября 2019

Я хочу написать такой класс:

class C c where
    op :: c -> c -> Bool

class A b => B b where
    func :: C c => b -> c -- ^ type 'c' is random(forall). 
    func2 :: b -> b -> Bool
    func2 x y = func b `op` func c

Здесь c - это тип, ограниченный C, и это ограничение будет использоваться в func2.Но это не может быть компилятором.Тип c не является реальным типом.Я пытаюсь добавить forall или использовать TypeFamilies, но никто из них не может этого сделать.TypeFamilies выглядит хорошо, но его нельзя использовать с ограничением в определении функции, например C c => b -> c или `type X x :: C * => *.

Должен ли я использовать (A b, C c) => B b c для определения этого класса?У меня есть другой класс с использованием B, как B b => D d b.Если добавить параметр для класса B, классу D нужен еще один параметр.Фактически, Seq a будет использоваться с классом D, который не может соответствовать D d b.

РЕДАКТИРОВАТЬ: еще одно описание.

{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE FlexibleInstances #-}
module Main where

type Ta = (Integer, Integer)
newtype Tb t = Tb { tb :: [t] } deriving Show

class Eq a => A a where
    a1f :: Ord b => a -> b
    a2f :: a -> a -> Bool
    a2f x y = a1f x >= a1f y

instance A Ta where
    a1f (_, y) = y

class A a => B b a where
    op :: b a -> b a

instance B Tb Ta where
    op x = x

main :: IO ()
main = putStrLn $ show $ op $ (Tb [(1, 1)] :: Tb Ta)

Компилятор будет пожаловаться на строку a2f :: b -> Bool:

    • Could not deduce (Ord a0) arising from a use of ‘>=’
      from the context: A a
        bound by the class declaration for ‘A’ at test.hs:10:15
      The type variable ‘a0’ is ambiguous
      These potential instances exist:
        instance Ord Ordering -- Defined in ‘GHC.Classes’
        instance Ord Integer
          -- Defined in ‘integer-gmp-1.0.2.0:GHC.Integer.Type’
        instance Ord a => Ord (Maybe a) -- Defined in ‘GHC.Maybe’
        ...plus 22 others
        ...plus four instances involving out-of-scope types
        (use -fprint-potential-instances to see them all)
    • In the expression: a1f x >= a1f y
      In an equation for ‘a2f’: a2f x y = a1f x >= a1f y

EDIT2: использовать семейства типов

...
class Eq a => A a where
    type AT a :: *
    a1f :: Ord (AT a) => a -> AT a
    a2f :: a -> a -> Bool
    a2f x y = a1f x >= a2f y

instance A Ta where
    type AT Ta = Integer
    a1f (_, y) = y
...

Будет отображаться ошибка с:

    • Could not deduce (Ord (AT a)) arising from a use of ‘>=’
      from the context: A a
        bound by the class declaration for ‘A’ at test.hs:10:15
    • In the expression: a1f x >= a1f y
      In an equation for ‘a2f’: a2f x y = a1f x >= a1f y

Ответы [ 2 ]

1 голос
/ 24 сентября 2019

Наименьшее исправление кода ваших семейств типов, позволяющее его компилировать, - это переместить требование на ограничение Ord из того места, где оно создается, в место его использования:

{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeSynonymInstances #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE ConstrainedClassMethods #-}

type Ta = (Integer, Integer)

class Eq a => A a where
    type AT a :: *
    a1f :: a -> AT a
    a2f :: Ord (AT a) => a -> a -> Bool
    a2f x y = a1f x >= a1f y

instance A Ta where
    type AT Ta = Integer
    a1f (_, y) = y

Если вынравится только требовать Ord (AT a), когда используется реализация по умолчанию, вы можете использовать DefaultSignatures (и исключить ConstrainedClassMethods):

{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeSynonymInstances #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE DefaultSignatures #-}

type Ta = (Integer, Integer)

class Eq a => A a where
    type AT a :: *
    a1f :: a -> AT a
    a2f :: a -> a -> Bool
    default a2f :: Ord (AT a) => a -> a -> Bool
    a2f x y = a1f x >= a1f y

instance A Ta where
    type AT Ta = Integer
    a1f (_, y) = y

Однако эта структура класса типов выходит за рамки странного и недиоматического.(Некоторые красные флаги, которые он поднимает, когда я читаю его: что это за ограничение Eq делает там? Почему существует класс только с одним экземпляром? Почему a2f внутри класса, а не снаружи? Почему не a1fпросто не-класс-полиморфная функция? Почему мы должны верить, что для каждого типа есть только одна каноническая функция выбора?)

Я хотел бы повторить, что вы должны рассказать нам больше о том, что goal вы пытаетесь достичь этого, а не говорите о предложенных вами классах типов для достижения этой цели.Многое об этой архитектуре кричит «новичок, пытающийся использовать классы типов так, как классы ОО используют классы», что станет для вас постоянным источником несоответствий импеданса и бумажных потертостей.Я сильно подозреваю, что вы просто не должны определять новый класс типов вообще.

1 голос
/ 23 сентября 2019

В вашем коде в том виде, в каком он есть, проблема в том, что c в func b `op` func c равно неоднозначно .Это не очень большая проблема: просто закрепите выбор местной подписью.Например,

func2 x y = func x `op` (func y :: Int)

Но это может быть не то, что вы действительно хотите.Должен ли c действительно быть параметром типа класса func или всего экземпляра?В последнем случае MPTC будет правильным подходом.

{-# LANGUAGE MultiParamTypeClasses, AllowAmbiguousTypes, TypeApplications #-}

class ∀ b c . (A b, C c) => B b c where
  func :: b -> c
  func2 :: b -> b -> Bool
  func2 x y = func @b @c b `op` func c

Или, если для каждого экземпляра имеет смысл только один c, тогда вам нужно семейство типов или fundep.

{-# LANGUAGE TypeFamilies #-}

class A b => B b where
  type Ct b :: *
  func :: b -> Ct b
  func2 :: b -> b -> Bool
  func2 x y = func b `op` func c
...