Написание монады Identity в терминах Free

В "Типы данных a la carte" Swierstra пишет, что с учетом Free (который он называет Term) и Zero вы можете реализовать монаду Identity:

data Term f a = Pure a
              | Impure (f (Term f a))
data Zero a

Term Zero теперь является монадой Identity. Я понимаю, почему это так. Проблема в том, что я никогда не могу использовать Term Zero как Monad из-за жесткого ограничения Functor f =>:

instance Functor f => Monad (Term f) where
    return x = Pure x
    (Pure x) >>= f = f x 
    (Impure f) >>= t = Impure (fmap (>>=f) t)

Как сделать Zero functor?

instance Functor Zero where
    fmap f z = ???

Кажется, здесь есть трюк: Поскольку Zero не имеет конструкторов, Impure никогда не может использоваться, поэтому случай Impure >>= никогда не вызывается. Это означает, что fmap никогда не вызывается, поэтому есть смысл, в котором это нормально:

instance Functor Zero where
    fmap f z = undefined

Проблема в том, что это похоже на обман. Что мне не хватает? Действительно ли Zero Functor? Или, может быть, Zero не является Функтором, и это является недостатком того, как мы выражаем Free в Haskell?

Ответ 1

Если вы включите DeriveFunctor, вы можете написать

data Zero a deriving Functor

но вы можете подумать об этом. Если вы хотите написать его самостоятельно, вы можете включить EmptyCase вместо этого, а затем написать фанк-выглядящий

instance Functor Zero where
    fmap f z = case z of

Ответ 2

Один из способов сделать это - использовать Data.Void вместо пустой декларации data, например:

import Data.Void

-- `Zero a` is isomorphic to `Void`
newtype Zero a = Zero Void

instance Functor Zero where
    -- You can promise anything if the precondition is that
    -- somebody gotta give you an `x :: Void`.
    fmap f (Zero x) = absurd x

См. этот вопрос для некоторых действительно замечательных объяснений того, что полезно для Void. Но основная идея заключается в том, что функция absurd :: Void -> a позволяет вам перейти от привязки can-never-happen x :: Void к любому типу, который вам нравится.

Ответ 3

Способом определения Zero a является следующее.

newtype Zero a = Zero (Zero a)

Другими словами, он кодирует вид глупых, слегка неочевидных утверждений о том, что есть фактически один способ получить значение Zero a: у вас уже есть один!

При этом определении absurd :: Zero a -> b определяется "естественным" способом

absurd :: Zero a -> b
absurd (Zero z) = absurd z

В некотором смысле эти определения являются законными, потому что они указывают точно, как их невозможно создать. Никакие значения Zero a не могут быть построены, если только кто-то еще не "обманывает".

instance Functor Zero where
  fmap f = absurd

Ответ 4

Еще один поворот на Luis Casillas answer заключается в том, чтобы полностью создать ваш тип из запасных частей:

type Id = Free (Const Void)

Экземпляр Functor для Const x будет работать по вашему желанию (его fmap ничего не делает, это просто отлично), и вам нужно будет позаботиться только при распаковке:

runId (Pure x) = x
runId (Free (Const ab)) = absurd ab

Все эти вещи, конечно, только "морально" эквивалентны Identity, потому что все они вводят дополнительные значения. В частности, мы можем различать

bottom
Pure bottom
Free bottom