Неоднозначное разрешение экземпляра в Haskell

Question

Введение и пример случая использования

Здравствуйте! У меня проблема в Haskell. Давайте рассмотрим следующий код:

class PolyMonad m1 m2 m3 | m1 m2 -> m3 where 
    polyBind :: m1 a -> (a -> m2 b) -> m3 b 

который просто объявляет о замене поли Монады. Хороший пример использование сценарий будет:

newtype Pure a = Pure { fromPure :: a } deriving (Show) 

instance PolyMonad Pure Pure Pure where 
    polyBind a f = f (fromPure a) 

instance PolyMonad Pure IO IO where 
    polyBind a f = f (fromPure a) 

instance PolyMonad IO Pure IO where 
    polyBind a f = (fromPure . f) <$> a 

instance PolyMonad IO IO IO where 
    polyBind a f = a >>= f 

и использовать его с -XRebindableSyntax как так:

test = do 
    Pure 5 
    print "hello" 
    Pure() 

, но мы можем сделать гораздо больше с ним - это только тест, чтобы показать вам пример дело.

Проблема

Давайте рассмотрим немного более сложное использование. Я хочу написать класс, похожий на полимонад, который не всегда будет выводить m3 b, но в некоторых конкретных случаях он будет выводить m3 (X b) для определенного X. Для простоты предположим, что мы хотим вывести m3 (X b) ТОЛЬКО, когда m1 или m2 был IO.

Кажется, мы не можем сделать это прямо сейчас в Haskell без потери гибкости. мне нужна следующие функции для компиляции без добавления какой-либо информации типа (код Haskell является сгенерированным):

tst1 x = x `polyBind` (\_ -> Pure 0) 
tst2 = (Pure 1) `polyBind` (\_ -> Pure 0) 
tst3 x y = x `polyBind` (\_ -> y `polyBind` (\_ -> Pure 0)) 

Во всяком случае эти функции компиляции хорошо используя PolyMonad класс.

Fundep попытка решить проблему

Одна из попыток может быть:

class PolyMonad2 m1 m2 m3 b | m1 m2 b -> out where 
    polyBind2 :: m1 a -> (a -> m2 b) -> out 

и, конечно, мы можем легко написать все необходимые экземпляры, такие как:

instance PolyMonad2 Pure Pure b (Pure b) where 
    polyBind2 a f = f (fromPure a) 

instance PolyMonad2 Pure IO b (IO (X b)) where 
    polyBind2 a f = fmap X $ f (fromPure a) 

-- ... 

, но наши тестовые функции не будут компилироваться при использовании polyBind2 вместо polyBind.Первая функция (tst1 x = x polyBind2 (\_ -> Pure 0)) выдает ошибку компиляции:

Could not deduce (PolyMonad2 m1 Pure b0 out) 
    arising from the ambiguity check for ‘tst1’ 
from the context (PolyMonad2 m1 Pure b out, Num b) 
    bound by the inferred type for ‘tst1’: 
      (PolyMonad2 m1 Pure b out, Num b) => m1 a -> out 
    at /tmp/Problem.hs:51:1-37 
The type variable ‘b0’ is ambiguous 
When checking that ‘tst1’ 
    has the inferred type ‘forall (m1 :: * -> *) b out a. 
         (PolyMonad2 m1 Pure b out, Num b) => 
         m1 a -> out’ 
Probable cause: the inferred type is ambiguous 

Закрытые семьи типа попытка решить проблему

немного лучше было бы использовать closed type families здесь, как:

class PolyMonad3 m1 m2 where 
    polyBind3 :: m1 a -> (a -> m2 b) -> OutputOf m1 m2 b 

type family OutputOf m1 m2 a where 
    OutputOf Pure Pure a = Pure a 
    OutputOf x y a = Pure (X a) 

, но затем при попытке скомпилировать функцию tst1 (tst1 x = x polyBind3) мы получаем другую ошибку компиляции времени:

Could not deduce (OutputOf m1 Pure b0 ~ OutputOf m1 Pure b) 
from the context (PolyMonad3 m1 Pure, Num b) 
    bound by the inferred type for ‘tst1’: 
      (PolyMonad3 m1 Pure, Num b) => m1 a -> OutputOf m1 Pure b 
    at /tmp/Problem.hs:59:1-37 
NB: ‘OutputOf’ is a type function, and may not be injective 
The type variable ‘b0’ is ambiguous 
Expected type: m1 a -> OutputOf m1 Pure b 
    Actual type: m1 a -> OutputOf m1 Pure b0 
When checking that ‘tst1’ 
    has the inferred type ‘forall (m1 :: * -> *) a b. 
         (PolyMonad3 m1 Pure, Num b) => 
         m1 a -> OutputOf m1 Pure b’ 
Probable cause: the inferred type is ambiguous 

Hacky попытки сделать это вокруг

Я нашел другое решение, но Hacky и в конце концов не работаю. Но это очень интересно. Давайте рассмотрим следующий тип класса:

class PolyMonad4 m1 m2 b out | m1 m2 b -> out, out -> b where 
    polyBind4 :: m1 a -> (a -> m2 b) -> out 

Конечно функциональная зависимость out -> b просто неправильно, потому что мы не можем определить такие случаи, как:

instance PolyMonad4 Pure IO b (IO (X b)) where 
    polyBind4 a f = fmap X $ f (fromPure a) 

instance PolyMonad4 IO IO b (IO b) where 
    polyBind4 = undefined 

но позволяет играть с ним и объявить их так (с помощью -XUndecidableInstances):

instance out~(Pure b) => PolyMonad4 Pure Pure b out where 
    polyBind4 a f = f (fromPure a) 

instance out~(IO(X b)) => PolyMonad4 Pure IO b out where 
    polyBind4 a f = fmap X $ f (fromPure a) 

instance out~(IO b) => PolyMonad4 IO IO b out where 
    polyBind4 = undefined 

instance out~(IO(X b)) => PolyMonad4 IO Pure b out where 
    polyBind4 = undefined 

Что забавно, некоторые из наших тестовых функций компилируется и работы, а именно:

tst1' x = x `polyBind4` (\_ -> Pure 0) 
tst2' = (Pure 1) `polyBind4` (\_ -> Pure 0) 

, но это не:

tst3' x y = x `polyBind4` (\_ -> y `polyBind4` (\_ -> Pure 0)) 

в результате компиляции ошибки времени:

Could not deduce (PolyMonad4 m3 Pure b0 (m20 b)) 
    arising from the ambiguity check for ‘tst3'’ 
from the context (PolyMonad4 m3 Pure b1 (m2 b), 
        PolyMonad4 m1 m2 b out, 
        Num b1) 
    bound by the inferred type for ‘tst3'’: 
      (PolyMonad4 m3 Pure b1 (m2 b), PolyMonad4 m1 m2 b out, Num b1) => 
      m1 a -> m3 a1 -> out 
    at /tmp/Problem.hs:104:1-62 
The type variables ‘m20’, ‘b0’ are ambiguous 
When checking that ‘tst3'’ 
    has the inferred type ‘forall (m1 :: * -> *) 
           (m2 :: * -> *) 
           b 
           out 
           a 
           (m3 :: * -> *) 
           b1 
           a1. 
         (PolyMonad4 m3 Pure b1 (m2 b), PolyMonad4 m1 m2 b out, Num b1) => 
         m1 a -> m3 a1 -> out’ 
Probable cause: the inferred type is ambiguous 

Еще более Hacky попытка использования NewType оберточной

Я сказал, что еще хаки, потому что это приводит нас к использованию -XIncoherentInstances, которые являются Just (Pure evil). Одна из идей, может быть, конечно, писать Newtype обертка:

newtype XWrapper m a = XWrapper (m (X (a))) 

и некоторые утилиты для распаковки его:

class UnpackWrapper a b | a -> b where 
    unpackWrapper :: a -> b 

instance UnpackWrapper (XWrapper m a) (m (X a)) where 
    unpackWrapper (XWrapper a) = a 

instance UnpackWrapper (Pure a) (Pure a) where 
    unpackWrapper = id 

instance UnpackWrapper (IO a) (IO a) where 
    unpackWrapper = id 

теперь мы можем Исли объявить следующие случаи:

instance PolyMonad Pure Pure Pure 
instance PolyMonad Pure IO (XWrapper IO) 
instance PolyMonad IO Pure (XWrapper IO) 
instance PolyMonad IO IO IO 

но опять же, мы не можем запускать наши тесты при объединении функций связывания и разворота:

polyBindUnwrap a f = unpackWrapper $ polyBind a f 

тестовые функции не скомпилируются снова. Мы можем здесь испортить -XIncoherentInstances (см. Список кодов в конце), но пока я не получил никаких хороших результатов.

Последний вопрос

Является ли это проблема, которая не может быть сделано с помощью текущей реализации GHC Haskell?

Полный листинг кода

Вот полный код листинга, который может быть запущен в GHC> = 7.8:

{-# LANGUAGE FlexibleInstances #-} 
{-# LANGUAGE FunctionalDependencies #-} 
{-# LANGUAGE TypeFamilies #-} 
{-# LANGUAGE UndecidableInstances #-} 

import Control.Applicative 

class PolyMonad m1 m2 m3 | m1 m2 -> m3 where 
    polyBind :: m1 a -> (a -> m2 b) -> m3 b 


---------------------------------------------------------------------- 
-- Some utils 
---------------------------------------------------------------------- 

newtype Pure a = Pure { fromPure :: a } deriving (Show) 
newtype X a = X { fromX :: a } deriving (Show) 

main = return() 

---------------------------------------------------------------------- 
-- Example use cases 
---------------------------------------------------------------------- 

instance PolyMonad Pure Pure Pure where 
    polyBind a f = f (fromPure a) 

instance PolyMonad Pure IO IO where 
    polyBind a f = f (fromPure a) 

instance PolyMonad IO Pure IO where 
    polyBind a f = (fromPure . f) <$> a 

instance PolyMonad IO IO IO where 
    polyBind a f = a >>= f 

-- works when using rebindable syntax 
--test = do 
-- Pure 5 
-- print "hello" 
-- Pure() 

tst1 x = x `polyBind` (\_ -> Pure 0) 
tst2 = (Pure 1) `polyBind` (\_ -> Pure 0) 
tst3 x y = x `polyBind` (\_ -> y `polyBind` (\_ -> Pure 0)) 

---------------------------------------------------------------------- 
-- First attempt to solve the problem 
---------------------------------------------------------------------- 


class PolyMonad2 m1 m2 b out | m1 m2 b -> out where 
    polyBind2 :: m1 a -> (a -> m2 b) -> out 


instance PolyMonad2 Pure Pure b (Pure b) where 
    polyBind2 a f = f (fromPure a) 

instance PolyMonad2 Pure IO b (IO (X b)) where 
    polyBind2 a f = fmap X $ f (fromPure a) 

-- ... 

-- tst1 x = x `polyBind2` (\_ -> Pure 0) -- does NOT compile 


---------------------------------------------------------------------- 
-- Second attempt to solve the problem 
---------------------------------------------------------------------- 

class PolyMonad3 m1 m2 where 
    polyBind3 :: m1 a -> (a -> m2 b) -> OutputOf m1 m2 b 

type family OutputOf m1 m2 a where 
    OutputOf Pure Pure a = Pure a 
    OutputOf x y a = Pure (X a) 

-- tst1 x = x `polyBind3` (\_ -> Pure 0) -- does NOT compile 


---------------------------------------------------------------------- 
-- Third attempt to solve the problem 
---------------------------------------------------------------------- 

class PolyMonad4 m1 m2 b out | m1 m2 b -> out, out -> b where 
    polyBind4 :: m1 a -> (a -> m2 b) -> out 


instance out~(Pure b) => PolyMonad4 Pure Pure b out where 
    polyBind4 a f = f (fromPure a) 

instance out~(IO(X b)) => PolyMonad4 Pure IO b out where 
    polyBind4 a f = fmap X $ f (fromPure a) 

instance out~(IO b) => PolyMonad4 IO IO b out where 
    polyBind4 = undefined 

instance out~(IO(X b)) => PolyMonad4 IO Pure b out where 
    polyBind4 = undefined 


tst1' x = x `polyBind4` (\_ -> Pure 0) 
tst2' = (Pure 1) `polyBind4` (\_ -> Pure 0) 
--tst3' x y = x `polyBind4` (\_ -> y `polyBind4` (\_ -> Pure 0)) -- does NOT compile 


---------------------------------------------------------------------- 
-- Fourth attempt to solve the problem 
---------------------------------------------------------------------- 

class PolyMonad6 m1 m2 m3 | m1 m2 -> m3 where 
    polyBind6 :: m1 a -> (a -> m2 b) -> m3 b 

newtype XWrapper m a = XWrapper (m (X (a))) 


class UnpackWrapper a b | a -> b where 
    unpackWrapper :: a -> b 

instance UnpackWrapper (XWrapper m a) (m (X a)) where 
    unpackWrapper (XWrapper a) = a 

instance UnpackWrapper (Pure a) (Pure a) where 
    unpackWrapper = id 

instance UnpackWrapper (IO a) (IO a) where 
    unpackWrapper = id 

--instance (a1~a2, out~(m a2)) => UnpackWrapper (m a1) out where 
-- unpackWrapper = id 


--{-# LANGUAGE OverlappingInstances #-} 
--{-# LANGUAGE IncoherentInstances #-} 

instance PolyMonad6 Pure Pure Pure where 
    polyBind6 = undefined 

instance PolyMonad6 Pure IO (XWrapper IO) where 
    polyBind6 = undefined 

instance PolyMonad6 IO Pure (XWrapper IO) where 
    polyBind6 = undefined 

instance PolyMonad6 IO IO IO where 
    polyBind6 = undefined 

--polyBind6' a f = unpackWrapper $ polyBind6 a f 

--tst1'' x = x `polyBind6'` (\_ -> Pure 0) 
--tst2'' = (Pure 1) `polyBind4` (\_ -> Pure 0) 
--tst3'' x y = x `polyBind4` (\_ -> y `polyBind4` (\_ -> Pure 0)) -- does NOT compile 

Answer 1

Я не думаю, что этот вопрос зависит от семей инъективными типа.

Биты семейства инъективных типов упоминаются в сообщении об ошибке вокруг закрытого типа семейства OutputOf. Но эта функция действительно не является инъективной - второе уравнение для нее допускает любые x и y. GHC любит напоминать пользователям о том, что он не анализирует эффективность инъекций для семейств типов, но иногда (например, здесь) это предупреждение не помогает.

Вместо этого проблемы, с которыми вы сталкиваетесь, похоже, связаны с перегруженными числами. Когда вы говорите Pure 0, GHC правильно вводит тип Num a => Pure a. Проблема в том, что функции типа уровня, к которым вы обращаетесь (тип разрешения класса, функциональные зависимости, семейства типов), очень сильно заботятся о том, какой конкретный выбор сделан для a. Например, вполне возможно, что любой из ваших подходов ведет себя по-другому для Int, чем для Integer. (Например, вы можете иметь различные экземпляры PolyMonad2 или дополнительных уравнений в OutputOf.)

Решение все это могло бы быть использование RebindableSyntax и определить fromInteger быть мономорфным, таким образом фиксируя числовой тип и избежать хлопот.

Answer 2

Я считаю, что принципиальное отличие в том, что здесь:

class PolyMonad m1 m2 m3 | m1 m2 -> m3 where 
    polyBind :: m1 a -> (a -> m2 b) -> m3 b 

b полностью полиморфный; это не параметр класса типа, поэтому экземпляр может быть выбран и функциональная зависимость применяется для определения m3 от m1 и m2 независимо от b. Он также появляется в двух местах; если тип inferencer знает тип результата или тип функции, переданной в polyBind, то он может достаточно определить b. И такой тип, как Num b => b, с удовольствием «пропустит» многие приложения polyBind, пока он не будет использоваться в месте, которое фиксирует конкретный тип. Хотя я думаю, что это может быть просто ограничение мономорфизма, по умолчанию использующее тип, который избавляет вас от неоднозначной ошибки переменной типа в этом случае (именно то, что она была предназначена для выполнения).

В то время как здесь:

class PolyMonad2 m1 m2 m3 b | m1 m2 b -> out where 
    polyBind2 :: m1 a -> (a -> m2 b) -> out 

b появляется в качестве параметра класса типа. Если мы попытаемся сделать вывод, что такое out, нам необходимо b, прежде чем мы сможем выбрать экземпляр.И нет причин для того, чтобы b нести какое-либо конкретное отношение к структуре типа out (точнее, это отношение может быть различным для каждого отдельного экземпляра, что в конечном итоге является тем, чего вы пытаетесь достичь), поэтому невозможно «следуйте за b через« цепочку polyBind2 звонков, если вы полностью не разрешили все экземпляров.

И если b является полиморфным число Num b => b и out ограничивается его использованием, чтобы быть в форме Num c => m c (для некоторого типа конструктора m), нет никаких оснований, что c и b должны быть жеNum пример. Таким образом, в прикованной серии polyBind2 вызовов, работающих на номерах, каждый промежуточный результат может использовать другой Num экземпляр, и, не зная ни одного из них нет никакого способа, чтобы выбрать правильные PolyMonad2 экземпляров, которые объединяют в b с чем-то в out. Тип defaulting применяется только в том случае, если все ограничения для переменной являются числовыми классами прелюдии, но здесь b участвует в ограничении PolyMonad2 m1 m2 m3 b, поэтому его нельзя использовать по умолчанию (что, вероятно, хорошо, поскольку именно тот тип, который вы выберете, может повлиять этот экземпляр используется и резко меняет поведение программы: только числовые классы, как известно, являются «приближениями» друг к другу, поэтому, если программа неоднозначна в отношении того, какой экземпляр использовать, то полуразмерно просто произвольно выбрать один а не жаловаться на двусмысленность).

То же действительно идет для любого метода для определения out из m1, m2 и b, насколько я знаю, является ли это функциональная зависимость, семьи типа, или что-то еще. Я не уверен, как на самом деле решить эту проблему здесь, не предоставляя больше аннотаций типа.