Содержит ли конструктор типов Both фантомный тип для левого/правого регистра?

Насколько я знаю, в Haskell только типы содержат значения, а не конструкторы типов. Either — это конструктор бинарного типа вида * -> * -> *. Left и Right оба применяют этот конструктор типа к одному типу, который предоставляется переданным значением. Не означает ли это, что в обоих случаях Either применяется лишь частично и, таким образом, остается конструктором типа, ожидающим отсутствующий аргумент типа?

let x = Right 'x' -- Either a Char

x имеет тип Either a Char. Я бы предположил, что этот тип будет иметь вид * -> *. Это явно полиморфный тип, а не наземный. Тем не менее, Either a Char может содержать такие значения, как 'x'.

Я подозреваю, что переменная типа a является фантомным типом для случая Right соответственно. b за Left. Я знаю фантомные типы в связи с Const, где соответствующая переменная типа вообще не используется. Я на правильном пути?


polymorphism haskell higher-kinded-types type-constructor
person Community    schedule 14.11.2017    source источник
comment
Either Char — это конструктор типа * -> *. Either Char a — это тип (типа *) — это сокращение от forall a . Either Char a; это должен быть тип, потому что каждый forall является типом (имеет вид *). Ни одна из переменных типа в Either a b не может быть фантомной, так как если у вас есть x :: Either a b, то внутри может содержаться a или может быть b; вы можете обнаружить, что a нет, только с помощью сопоставления с образцом.   -  person user2407038    schedule 15.11.2017

Ответы (3)


arrow_upward
8
arrow_downward

Насколько я знаю, в Haskell только типы содержат значения, а не конструкторы типов.

Точно.

Left и Right оба применяют этот конструктор типов к одному типу

Вы не можете этого сказать. Left и Right вообще не живут в языке типов, поэтому они ничего не применяют ни к каким типам, они применяются только к значениям.

x имеет тип Either a Char. Я бы предположил, что этот тип будет иметь вид * -> *

Вам нужно различать аргументы функции/конструктора и переменные типа. По сути, это различие между свободными и связанными переменными. Either a Char по-прежнему имеет вид *, а не * -> *, потому что он уже применяется к a. Да, это переменная типа, но это уже уже примененный аргумент.

Тем не менее, Either a Char может содержать такие значения, как 'x'.

Не совсем — его можно населить такими значениями, как Right 'x'.

Я подозреваю, что переменная типа a является фантомным типом для случая Right соответственно. b для Left

своего рода, но я бы не назвал это «призраком», потому что вы не можете просто сосчитать Left или Right. По крайней мере, если вы не выберете Either Void b, но в этом случае у вас нет переменной a.

person leftaroundabout    schedule 14.11.2017
comment
Я все еще пытаюсь это понять. Either a Char — это монотип или константа типа, а a — просто заполнитель для определенного типа. Какой тип a заменяется, зависит от контекста, например. let t = Right 'x' имеет тип Either Bool Char в контексте [Left True, t, Left False]. Это правильное рассуждение? - person ; 24.11.2017
comment
Да, это об этом. - person leftaroundabout; 24.11.2017

arrow_upward
1
arrow_downward

Я бы сказал, что переменная типа является фантомной тогда и только тогда, когда выбор переменной типа не ограничивает, какие значения могут быть переданы конструкторам типа. Важной частью является то, что это определение ориентировано на тип. Это определяется просмотром только определения типа, а не какого-то конкретного значения типа.

Так имеет ли значение, что значение типа String не появляется в значении Left 5 :: Either Int String? Нисколько. Важно то, что выбор String в Either Int String предотвращает проверку типов Right ().

person Carl    schedule 14.11.2017

arrow_upward
1
arrow_downward

Haskell имеет «неявную универсальную количественную оценку», что означает, что переменные типа имеют неявную forall. Either a Int эквивалентно forall a. Either a Int.

Один из способов рассмотрения forall состоит в том, что это похоже на лямбду, но для переменных типа. Если мы используем синтаксис @ для приложения типа, то вы можете «применить» тип к этому и получить новый тип.

let foo = Right 1 :: forall a. Either a Int
foo @Char   :: Either Char Int
foo @Double :: Either Double Int
person ephrion    schedule 14.11.2017