Как составить "более свободные" эффекты в haskell?

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

Я использую только эффекты State и Fresh. Я использую два состояния, и мой бегун эффекта выглядит следующим образом:

Кроме того, я определил функцию FindMacro с этим типом:

Все это пока работает отлично. Проблема возникает, когда я пытаюсь написать macroexpand2 (ну, macroexpand1, но я упрощаю это, так что вопрос проще следовать):

Хорошо, я могу добавить аннотацию Members к типу:

Мне посоветовали на irc попробовать forall r v w., который не имел никакого значения. Из любопытства я попытался использовать IncoherentInstances при компиляции этого кода (я не хотел проверять вилку более свободной и игры), чтобы узнать, может ли это дать мне ключ к тому, что происходит. Это не так:

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

Ответы

Ответ 1

Тип вывода для расширяемых эффектов был исторически плохим. Рассмотрим некоторые примеры:

{-# language TypeApplications #-}

-- mtl
import qualified Control.Monad.State as M

-- freer
import qualified Control.Monad.Freer as F
import qualified Control.Monad.Freer.State as F

-- mtl works as usual
test1 = M.runState M.get 0

-- this doesn't check
test2 = F.run $ F.runState F.get 0  

-- this doesn't check either, although we have a known
-- monomorphic state type
test3 = F.run $ F.runState F.get True

-- this finally checks
test4 = F.run $ F.runState (F.get @Bool) True

-- (the same without TypeApplication)
test5 = F.run $ F.runState (F.get :: F.Eff '[F.State Bool] Bool) True

Я попытаюсь объяснить общую проблему и предоставить минимальную иллюстрацию кода. Автономная версия кода может быть найдена здесь.

На самом базовом уровне (без учета оптимизированных представлений) Eff определяется следующим образом:

{-# language
  GADTs, DataKinds, TypeOperators, RankNTypes, ScopedTypeVariables,
  TypeFamilies, DeriveFunctor, EmptyCase, TypeApplications,
  UndecidableInstances, StandaloneDeriving, ConstraintKinds,
  MultiParamTypeClasses, FlexibleInstances, FlexibleContexts,
  AllowAmbiguousTypes, PolyKinds
  #-}

import Control.Monad

data Union (fs :: [* -> *]) (a :: *) where
  Here  :: f a -> Union (f ': fs) a
  There :: Union fs a -> Union (f ': fs) a

data Eff (fs :: [* -> *]) (a :: *) =
  Pure a | Free (Union fs (Eff fs a))

deriving instance Functor (Union fs) => Functor (Eff fs)

Другими словами, Eff является свободной монадой из объединения списка функторов. Union fs a ведет себя как n-ary Coproduct. Бинарный Coproduct похож на Either для двух функторов:

data Coproduct f g a = InL (f a) | InR (g a)

Напротив, Union fs a позволяет выбрать функтор из списка функторов:

type MyUnion = Union [[], Maybe, (,) Bool] Int

-- choose the first functor, which is []
myUnion1 :: MyUnion
myUnion1 = Here [0..10]

-- choose the second one, which is Maybe
myUnion2 :: MyUnion
myUnion2 = There (Here (Just 0))

-- choose the third one
myUnion3 :: MyUnion
myUnion3 = There (There (Here (False, 0)))

В качестве примера реализуем эффект State. Во-первых, нам нужно иметь экземпляр Functor для Union fs, так как Eff имеет экземпляр Monad, если Functor (Union fs).

Functor (Union '[]) является тривиальным, так как пустое объединение не имеет значений:

instance Functor (Union '[]) where
  fmap f fs = case fs of {} -- using EmptyCase

В противном случае мы добавим функтор к объединению:

instance (Functor f, Functor (Union fs)) => Functor (Union (f ': fs)) where
  fmap f (Here fa) = Here (fmap f fa)
  fmap f (There u) = There (fmap f u)

Теперь определение State и бегунов:

run :: Eff '[] a -> a
run (Pure a) = a

data State s k = Get (s -> k) | Put s k deriving Functor

runState :: forall s fs a. Functor (Union fs) => Eff (State s ': fs) a -> s -> Eff fs (a, s)
runState (Pure a)                 s = Pure (a, s)
runState (Free (Here (Get k)))    s = runState (k s) s
runState (Free (Here (Put s' k))) s = runState k s'
runState (Free (There u))         s = Free (fmap (`runState` s) u)

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

action1 :: Eff '[State Int] Int
action1 =
  Free $ Here $ Get $ \s ->
  Free $ Here $ Put (s + 10) $
  Pure s

-- multiple state
action2 :: Eff '[State Int, State Bool] ()
action2 =
  Free $ Here $ Get $ \n ->            -- pick the first effect
  Free $ There $ Here $ Get $ \b ->    -- pick the second effect
  Free $ There $ Here $ Put (n < 10) $ -- the second again
  Pure ()

Сейчас:

> run $ runState action1 0
(0,10)
> run $ (`runState` False) $ (`runState` 0) action2
(((),0),True)

Здесь всего две недостающие вещи.

Первый - это экземпляр monad для Eff, который позволяет использовать do -notation вместо Free и Pure, а также позволяет использовать много полиморфных монадических функций. Мы пропустим его здесь, потому что это просто написать.

Второй - это вывод/перегрузка для выбора эффектов из списков эффектов. Раньше нам нужно было написать Here x, чтобы выбрать первый эффект, There (Here x), чтобы выбрать второй, и так далее. Вместо этого мы хотели бы написать код, который является полиморфным в списках эффектов, поэтому все, что мы должны указать, - это то, что какой-то эффект является элементом списка, а некоторые скрытые магии типа typeclass вставляют соответствующее количество There -s.

Нам нужен класс Member f fs, который может вставлять f a -s в Union fs a -s, когда f является элементом fs. Исторически сложилось так, что люди реализовали это двумя способами.

Сначала, непосредственно с помощью OverlappingInstances:

class Member (f :: * ->  *) (fs :: [* -> *]) where
  inj :: f a -> Union fs a

instance Member f (f ': fs) where
  inj = Here

instance {-# overlaps #-} Member f fs => Member f (g ': fs) where
  inj = There . inj

-- it works
injTest1 :: Union [[], Maybe, (,) Bool] Int
injTest1 = inj [0]

injTest2 :: Union [[], Maybe, (,) Bool] Int
injTest2 = inj (Just 0)

Во-вторых, косвенно, сначала вычислив индекс f в fs с семейством типов, а затем реализуя inj с неперекрывающимся классом, руководствуясь индексом f -s. Обычно это рассматривается как лучше, потому что люди склонны не любить перекрывающиеся экземпляры.

data Nat = Z | S Nat

type family Lookup f fs where
  Lookup f (f ': fs) = Z
  Lookup f (g ': fs) = S (Lookup f fs)

class Member' (n :: Nat) (f :: * -> *) (fs :: [* -> *]) where
  inj' :: f a -> Union fs a

instance fs ~ (f ': gs) => Member' Z f fs where
  inj' = Here

instance (Member' n f gs, fs ~ (g ': gs)) => Member' (S n) f fs where
  inj' = There . inj' @n

type Member f fs = Member' (Lookup f fs) f fs

inj :: forall fs f a. Member f fs => f a -> Union fs a
inj = inj' @(Lookup f fs)

-- yay
injTest1 :: Union [[], Maybe, (,) Bool] Int
injTest1 = inj [0]

Библиотека freer использует второе решение, а extensible-effects использует первый вариант для версий GHC старше 7,8, а второй для новых GHC-систем.

В любом случае оба решения имеют одно и то же ограничение вывода, а именно, что почти всегда Lookup можно использовать только конкретные мономорфные типы, а не типы, содержащие переменные типа. Примеры в ghci:

> :kind! Lookup Maybe [Maybe, []]
Lookup Maybe [Maybe, []] :: Nat
= 'Z

Это работает, потому что нет переменных типа в Maybe или [Maybe, []].

> :kind! forall a. Lookup (Either a) [Either Int, Maybe]
forall a. Lookup (Either a) [Either Int, Maybe] :: Nat
= Lookup (Either a) '[Either Int, Maybe]

Этот зацикливается, потому что переменная типа a блокирует тип.

> :kind! forall a. Lookup (Maybe a) '[Maybe a]
forall a. Lookup (Maybe a) '[Maybe a] :: Nat
= Z

Это работает, потому что единственное, что мы знаем о переменных типа, состоит в том, что они равны сами по себе, а a равно a.

В общем случае, семейная редукция зацикливается на переменных, потому что решение ограничений может потенциально доработать их позже для разных типов, поэтому GHC не может делать никаких предположений о них (кроме того, что они равны сами по себе). По существу такая же проблема возникает при реализации OverlappingInstances (хотя семейств типов нет).

Позвольте вернуться к просмотру freer в свете этого.

import Control.Monad.Freer
import Control.Monad.Freer.State

test1 = run $ runState get 0 -- error

GHC знает, что у нас есть стек с единственным эффектом, так как run работает на Eff '[] a. Он также знает, что этот эффект должен быть State s. Но когда мы пишем get, GHC знает только, что он имеет эффект State t для некоторой свежей переменной t и что Num t должен выполняться, поэтому, когда он пытается вычислить эквивалент freer Lookup (State t) '[State s], он застревает в переменных типа, и любое последующее разрешение экземпляра срабатывает на выражение типа застрявшего типа. Другой пример:

foo = run $ runState get False -- error

Это также терпит неудачу, потому что GHC нужно вычислить Lookup (State s) '[State Bool], и хотя мы знаем, что состояние должно быть Bool, это все еще застревает из-за переменной s.

foo = run $ runState (modify not) False -- this works

Это работает, потому что тип состояния modify not может быть разрешен до Bool, а Lookup (State Bool) '[State Bool] уменьшается.

Теперь, после этого большого объезда, я рассмотрю ваши вопросы в конце вашего сообщения.

Overlapping instances не указывает на какое-либо возможное решение, просто артефакт ошибки типа. Мне нужно больше контекста кода, чтобы точно определить, как именно он возникает, но я уверен, что это не актуально, так как как только Lookup застревает, дело становится безнадежным.
IncoherentInstances также не имеет значения и не помогает. Нам нужен конкретный индекс положения эффекта, чтобы иметь возможность генерировать код для программы, и мы не можем вывести индекс из воздуха, если Lookup застрял.
Проблема с findMacro заключается в том, что она имеет State эффекты с переменными типа внутри состояний. Всякий раз, когда вы хотите использовать findMacro, вы должны убедиться, что параметры v и w для Scope и Global являются известными конкретными типами. Вы можете сделать это с помощью аннотаций типа или более удобно использовать TypeApplications и написать findMacro @Int @Int для указания v = Int и w = Int. Если у вас есть findMacro внутри полиморфной функции, вам нужно включить ScopedTypeVariables, bind v и w с помощью аннотации forall v w. для этой функции и написать findMacro @v @w при ее использовании. Вам также необходимо включить {-# language AllowAmbiguousTypes #-} для полиморфных v или w (как указано в комментариях). Я думаю, что в GHC 8 это разумное расширение для включения вместе с TypeApplications.

Приложение:

Однако, к счастью, новые функции GHC 8 позволяют нам восстанавливать вывод типа для расширяемых эффектов, и мы можем заключить, что все mtl может, а также некоторые вещи mtl не могут обрабатывать. Новый вывод типа также инвариантен относительно упорядочения эффектов.

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