Тип данных с ограничением типа в Wadler - статья Суть функционального программирования,

В статье Фила Уодлера «Сущность функционального программирования» Уодлер описывает применение монад с помощью простой программы-интерпретатора. Программа показана ниже:

Терм — это переменная, константа, сумма, лямбда-выражение или приложение. Следующее будет служить тестовыми данными.

term0 = (App (Lam "x" (Add (Var "x") (Var "x"))) (Add (Con 10) (Con 11)))

Для наших целей монада — это тройка (M,unitM,bindM), состоящая из конструктора типа M и пары полиморфных функций.

unitM :: a -> M a
bindM :: M a -> (a -> M b) -> M b

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

type Name = String

data Value = Wrong
           | Num Int
           | Fun (Value -> M Value)

Я не понимаю, как сюда попало M Value. Насколько я понимаю, Haskell не допускает ограничений типов для конструкторов типов данных?

Дополнительная информация: Полная программа приведена ниже:

type Name = String
data Term = Var Name
          | Con Int
          | Add Term Term
          | Lam Name Term
          | App Term Term
data Value = Wrong
           | Num Int
           | Fun (Value -> M Value)
type Environment = [(Name, Value)]
interp :: Term -> Environment -> M Value
interp (Var x) e = lookup x e
interp (Con i) e = unitM (Num i)
interp (Add u v) e = interp u e `bindM` (\a ->
                                            interp v e `bindM` (\b ->
                                                                  add a b))
interp (Lam x v) e = unitM (Fun (\a -> interp v ((x,a):e)))
interp (App t u) e = interp t e `bindM` (\f ->
                                             interp u e `bindM` (\a ->
                                                                     apply f a))

lookup :: Name -> Environment -> M Value
lookup x [] = unitM Wrong
lookup x ((y,b):e) = if x==y then unitM b else lookup x e

add :: Value -> Value -> M Value
add (Num i) (Num j) = unitM (Num (i+j))
add a b = unitM Wrong

apply :: Value -> Value -> M Value
apply (Fun k) a = k a
apply f a = unitM Wrong

Как видно, interp (Lam x v) e = unitM (Fun (\a -> interp v ((x,a):e))) требует определения data Value = ... | Func (Value -> M Value)

Я пытался реализовать interp (Lam x v) с помощью data Value = ... | Func (Value -> Value), но мне это не показалось возможным.


person coder_bro    schedule 22.09.2018    source источник
comment
Предполагается, что М следует заменить на I, E, P, S, O, L, ..., определенные позже в статье.   -  person Will Ness    schedule 22.09.2018


Ответы (1)


M не является ограничением, это конструктор типа. Таким образом, запись M Value аналогична [Value], Maybe Value и т. д. Ограничение будет чем-то вроде Monad m => m Value, где m — это переменная типа, а не конструктор типа, а Monad m — это ограничение (Monad — это класс типа).

В статье определение типа M value не было представлено, и позже показано, что вы можете дать ему разные определения (определения будут включать определение data M v = ... и функций bindM и unitM).

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

data Value m = Wrong
             | Num Int
             | Fun (Value m -> m (Value m))

И затем есть ограничение в типах функций, например:

interp :: Monad m => Term -> Environment -> m (Value m)
person Jonas Duregård    schedule 22.09.2018
comment
Понятно, так что в основном он использует функции bindM и unitM для представления монад, а не класса Monad m. Мне интересно, есть ли способ добиться того же, используя класс Monad m.. определение - person coder_bro; 22.09.2018
comment
Похоже, это не работает: значение данных m = Wrong | Целое число | Func (Value -> m Value): Ожидается еще один аргумент для 'Value' Ожидается тип, но 'Value' имеет вид '(k0 -> *) -> *' • В типе '(Value -> m Value) ' В определении конструктора данных 'Func' В объявлении данных для 'Value' | 13 | | Func (Значение -> Значение m) - person coder_bro; 22.09.2018
comment
Должно быть Fun (Value m -> m (Value m) - person chi; 22.09.2018