Как сделать это альтернативное определение, возможно, работать?

Question

Я hvae только invended следующее альтернативное определение Maybe:

type Maybe' a = forall b. (b -> (a -> b) -> b) 

just :: a -> Maybe' a 
just a = \d f -> f a 

nothing :: Maybe' a 
nothing = const 

bind :: Maybe' a -> (a -> Maybe' b) -> Maybe' b 
bind ma f = ma nothing (\a -> f a) 

Проблема в том, что я не могу добавить следующую декларацию экземпляр

instance Monad (Maybe') where 
    return = just 
    a >>= f = bind a f 

Сообщение об ошибке:

Type synonym Maybe' should have 1 argument, but has been given none 

Есть ли способ исправить?

Answer 1

Вы можете сделать это только для примера Monad, если вы обернете его в newtype. Вы также должны использовать PolymorphicComponents расширение (ослабленная форма RankNTypes) универсально количественного определения b:

{-# LANGUAGE PolymorphicComponents #-} 

newtype Maybe' a = Maybe' { unMaybe' :: forall b. (b -> (a -> b) -> b) } 

just :: a -> Maybe' a 
just a = Maybe' (\d f -> f a) 

nothing :: Maybe' a 
nothing = Maybe' const 

bind :: Maybe' a -> (a -> Maybe' b) -> Maybe' b 
bind ma f = Maybe' (unMaybe' ma const (\a -> unMaybe' (f a))) 

instance Monad Maybe' where 
    return = just 
    (>>=) = bind 

Причина вам нужно Newtype, что синонимы типа Haskell не «палка». Когда Haskell пытается сопоставить подпись типа Maybe' без newtype против класса класса Monad, он вообще не видит Maybe' и вместо этого видит необработанный базовый тип функции.

Haskell использует «основные типы», чтобы гарантировать, что каждый тип имеет нормальную форму. Нормальная форма основной функции:

(->) b ((->) ((->) a b) b) 

Синонимы типа не меняют нормальную форму типа, но Newtypes делать. В частности, newtype в этом случае перестраивает тип, так что нормальная форма теперь имеет номер a, так как требуется последний параметр типа, например, Monad.

Answer 2

Типичные синонимы не являются типами. С newtype вы получаете тип * -> *, а с синонимами типа вы этого не делаете. Поэтому ваш вопрос теперь сводится к тому, почему синонимы типов не являются первоклассными.

Ответ, вероятно, объясняется тем, что синонимы первого класса создавали бы слишком много двусмысленностей и делали бы вывод типа невозможным в простых случаях.

type First a b = (a, b) 
type Second a b = (b, a) 
type Both a = (a, a) 

Если мы можем определить Functor (First a), Functor (Second a) и Functor (Both a) экземпляров, то fmap (+1) (2, 3) будет Неоднозначный.

Ваше изобретение, BTW, называется Church encoding. Церковью можно закодировать что угодно. См. https://gist.github.com/rampion/2176199 для реализации нескольких кодировок в Haskell (пары, возможно и списки).

Answer 3

Синонимы типов не могут быть частично применены.

Синоним типа - это всего лишь короткая рука, чтобы помочь программисту, а не то, что на самом деле существует, как о чем говорит язык Haskell. Единственный способ, которым Haskell может иметь дело с синонимом типа, - это «просмотреть» его, чтобы увидеть тип с правой стороны. Параметры просто дают вам своего рода «макроязык».

Так Maybe' a точно соответствует forall b. (b -> (a -> b) -> b). Он ведет себя так же, как если бы вы написали forall b. (b -> (a -> b) -> b). Но что такое Maybe' самостоятельно без аргумента?Haskell не может справиться с этим как Maybe', ему придется заменить его чем-то другим. Но что? Если бы это означало что-нибудь, это должно было бы быть чем-то вроде \a ~> (forall b. (b -> (a -> b) -> b), где я использую \a ~> ... в качестве псевдосинтакса для лямбда уровня уровня; произвольная функция от типа к другому типу. Причина, по которой мне пришлось составлять синтаксис, заключается в том, что у Haskell нет синтаксиса для этого, и причина, по которой у него нет синтаксиса, заключается в том, что он не может обрабатывать полностью общие функции уровня.

Я не уверен, что поддержка произвольных ямбдов типа типа (типа конструкторов и семейств типов фактически очень ограниченных форм этого) была бы фактически невозможна, но это, безусловно, очень сложно. Таким образом, синонимы типов не могут быть частично применены.

Чтобы получить что-то, что можно сделать экземпляром Monad (который нужно что-то, что может быть применен к типу, чтобы сделать что-то типа - доброго * -> *), вам нужно использовать data или newtype создать конструктор типа. Синоним типа не может использоваться для этой цели.