Являются ли типы высшего порядка * действительно * типами в Haskell? Или они просто обозначают коллекции * конкретных * типов и ничего более?

Парамаметрически полиморфные функции

Рассмотрим следующую функцию:

f :: a -> Int
f x = (1 :: Int)

Мы могли бы сказать, что тип f - это a -> Int, и, следовательно, f имеет "полиморфный" тип.

Что из следующего является наиболее точным способом думать о f?

  1. Фактически существует сингл f типа a -> Int. Однако его можно использовать как f :: Int -> Int, как f :: Double -> Int и так далее.

  2. Буквально говоря, тип f НЕ a -> Int. В самом деле, это всего лишь сокращенный способ обозначить, что существует семейство функций f, чей тип конкретен (т. Е. Существует f :: Int -> Int, f :: Double -> Double и т. Д.; Более того, каждая из этих функций отличается друг от друга).

Высшие родственные типы

Точно так же мы можем рассмотреть следующее объявление типа:

data Maybe a = Just a | Nothing

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

  1. Не существует одиночного типа Maybe; действительно, существует просто семейство конкретных типов (Maybe Int, Maybe String и т. д.) и ничего более.

  2. Существует фактически единственный тип Maybe. Этот тип относится к более высокородным. Когда мы говорим, что это «тип», мы имеем в виду буквально (не как сокращение для (1)). Так уж получилось, что мы также можем написать Maybe Int, Maybe Double и т. Д. Для создания различных типов (которые оказываются конкретными). Но, в конце концов (т.е.): Maybe, Maybe Int и Maybe String обозначают три различных типа, два из которых являются конкретными, а один - более высокородным.

Резюме вопроса

В Haskell, действительно ли «высокодородные типы» являются типами? Или «настоящими типами» являются только конкретные типы, и когда мы говорим о «высокодородных типах», мы просто обозначаем семейство конкретных типов. Более того, парамаметрически полиморфные функции обозначают функции одного типа или они просто обозначают коллекцию функций конкретных типов (и не более того)?


types parametric-polymorphism haskell higher-kinded-types
person George    schedule 22.05.2016    source источник

Ответы (2)


arrow_upward
12
arrow_downward

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

Параметрически полиморфные функции

f действительно имеет тип f :: forall a.a->int

Это совершенно допустимый тип функции в типизированном лямбда-исчислении, на котором основан Haskell. Это может быть что-то вроде:

f = λa:Type.λx:a.(body for f)

Как получить от этого Double->Int? Вы примените его к Double типу:

f Double = (λa:Type.λx:a.(body for f)) Double => λx:Double.(body for f|a=Double)

Haskell выполняет обе операции (абстракцию типа и приложение типа) за сценой, хотя можно явно указать forall часть в сигнатуре типа с XExplicitForAll расширением GHC и явно создать Double->Int экземпляр f с сигнатурой типа:

f_double :: Double -> Int
f_double = f

Высшие типы

Рассмотрим простой тип:

data Example = IntVal Int | NoVal

(Да, это Maybe Int).

Maybe является конструктором типа, так же как IntVal является конструктором данных. Это в точности то же самое, только «на один уровень выше» в том смысле, что Maybe применяется к Type, так же как IntVal применяется к Int.

В лямбда-исчислении Maybe имеет тип:

Maybe : Type->Type

Haskell не позволяет вам получить тип из конструктора типов, но позволяет получить вид (это просто причудливое название для типа типа):

:k Maybe
Maybe :: * -> *

Так что нет, Maybe не является типом: у вас не может быть объекта с типом Maybe. Maybe - это (почти) функция от типов к типам, например IntVal - это функция от значений к значениям.

Мы называем результат применения Maybe к String как Maybe String, как мы называем результат применения IntVal к 4 как IntVal 4.

person Community    schedule 22.05.2016
comment
Если Maybe a не является типом, то как он может быть членом класса типов Monad? Я думал, например, что было бы неверно сказать, что конкретный Maybe (скажем, Maybe Int) является монадой. Действительно, Maybe Int не монада, но Maybe a монада. Итак, мой вопрос из вашего ответа таков: какие именно члены классов типов? Типы? Конструкторы типов? - person George; 22.05.2016
comment
По сути, ваш ответ заставляет меня понять, что типы отличаются от конструкторов типов (хотя они часто имеют одно и то же имя). Я понимаю, что классы типов имеют в качестве членов не типы, а конструкторы типов. Так ли это? - person George; 22.05.2016
comment
@George, члены классов типов - это вещи. :k Monad сообщает, что Monad ожидает (*->*) в качестве аргумента (и Maybe именно такой вид вещи). Но :k Num, например, ожидает *, поэтому Maybe не может быть членом Num (но Maybe Int может) - person ; 22.05.2016
comment
@George: (1) Когда мы говорим свободно, тип означает что-то вроде всего, что может существовать только справа от ::, возможно, за исключением классов / ограничений типов; когда мы говорим четко, тип означает все доброе *. (2) Классы типов могут содержать типы или конструкторы типов или что-нибудь еще! Eq имеет вид * -> Constraint, но Functor имеет вид (* -> *) -> Constraint. Люди привыкли называть такие вещи, как Functor, классами-конструкторами, чтобы различать их, но это использование в основном вышло из употребления. [продолжение…] - person Antal Spector-Zabusky; 22.05.2016
comment
@ Джордж: [… продолжение] И, наконец, (3) Maybe a не монада; Maybe - это монада. Только добрые вещи * -> * могут быть монадами! И Maybe a относится к типу * (или имеет ошибку области действия, если a не входит в область действия.) - person Antal Spector-Zabusky; 22.05.2016
comment
Я бы сказал, что часто бывает полезно не различать типы и конструкторы типов, если нет особо веской причины, по той же причине, что и не различать функции и (нефункциональные) значения. Я бы сказал, что это особенно актуально, когда используются PolyKinds или (в GHC 8) TypeInType. С PolyKinds вы можете иметь как Proxy :: Proxy Int, так и Proxy :: Proxy []. TypeInType удаляет различие между типами и видами, поэтому * -> * сам становится типом (начиная с * -> * :: *, который вы можете увидеть здесь: Just 1 :: (Maybe :: ((* -> *) :: *)) Int). - person David Young; 24.05.2016

arrow_upward
6
arrow_downward

Сначала вопрос: является ли утверждение «все списки имеют длину» одним оператором или серией операторов «список1 имеет длину», «список2 имеет длину», ...?

Если вы укажете тип f с явным forall, вы получите f :: forall a. a -> Int. Во-первых, это не «высшие». В GHCI мы можем делать следующее:

λ> :set -XRankNTypes
λ> :k (forall a. a -> Int)
(forall a. a -> Int) :: *

Итак, f имеет вид *.

Теперь в Haskell мы можем использовать ~ для проверки равенства типов. Мы можем установить следующее, чтобы проверять данные в GHCI:

λ> :set -XImpredicativeTypes
λ> :set -XTypeFamilies
λ> :t undefined :: ((~) Int Int) => a
undefined :: ((~) Int Int) => a :: a

Это показывает, что GHC вычислил равенство типов для этого примера. Неравенство типов даст следующую ошибку:

λ> undefined :: ((~) (Int -> Int) (Int)) => a

<interactive>:22:1:
    Couldn't match expected type ‘Int’ with actual type ‘Int -> Int’
    In the expression: undefined :: ((~) (Int -> Int) (Int)) => a
    In an equation for ‘it’:
    it = undefined :: ((~) (Int -> Int) (Int)) => a

Использование этого метода напрямую не позволит нам сравнивать тип f, но я нашел небольшой вариант, который должен работать для наших целей:

λ> :t undefined :: forall a. ((a -> Int) ~ (Int -> Int)) => a
undefined :: forall a. ((a -> Int) ~ (Int -> Int)) => a :: Int

Другими словами, если f эквивалентен типу g :: Int -> Int, тогда a должен быть Int. Это похоже на x = y, y = 0, поэтому x = 0. У нас не будет x = 0, пока мы не укажем y = 0, до тех пор у нас будет только x = y.

Maybe отличается тем, что имеет следующий вид:

λ> :k Maybe
Maybe :: * -> *

Поскольку мы используем DataKinds, у нас есть :k (~) :: k -> k -> GHC.Prim.Constraint, поэтому мы можем делать такие вещи, как:

λ> :t undefined :: (~) Maybe Maybe => Int
undefined :: (~) Maybe Maybe => Int :: Int

λ> :k Either ()
Either () :: * -> *

λ> :t undefined :: (~) Maybe (Either ()) => Int
Couldn't match expected type ‘Either ()’ with actual type ‘Maybe’

Подводя итог, f :: forall a. a -> Int имеет такой же смысл, как и утверждение «если вы дадите мне что-нибудь, я дам вам Int». Не могли бы вы перевести это утверждение в кучу утверждений «если вы дадите мне собаку…», «если вы дадите мне пенни…»? Да, но это ослабляет утверждение. В конце решите, что именно вы подразумеваете под «одинаковым», и вы получите свой ответ.

person Michael Klein    schedule 22.05.2016