Haskell - полиморфизм и значение в зависимости от типов

Question

От чтения статьи в Википедии для lambda cube и это thread, когда применяются к Haskell, я понимаю, что

1. семейства терминов проиндексированных терминов - типичная функции от значения дорожить
2. семейство терминов, индексированных по типам - ???
3. семейства типов проиндексированных типов - параметрический полиморфизм в конструкторах типа, семьи типа
4. семейства типов проиндексированных терминов - типы пи (в которых вы фальшивке с одноплодными типами в Haskell), типами сигмы, и т.д. ...

Пожалуйста, исправьте меня, если я привел приведенные выше примеры неправильно. Цитирование из этой статьи Википедии:

• Условия в зависимости от типа, или полиморфизм. Система F, так же как и лямбда-исчисление второго порядка (записанная как λ2 на диаграмме), получается путем наложения только этого свойства.

Я не знаю, как Haskell вписывается в эту (2) сверху. У Haskell есть сильное различие между терминами и типами и стирание типа, поэтому у вас нет элементов отражения в ООП, таких как typeof(a) или b.GetType(), а затем приступайте к возврату некоторого значения на основе информации о типе во время выполнения.

Так что единственное, что я могу думать в Haskell, относящиеся к (2), может быть,

• Возвращение типа полиморфизма скажем mempty в Data.Monoid, где величина зависит от типа экземпляра
• семейства данных, где вы берете типы на LHS и имеете конструкторы стоимости на RHS

Будет ли это правильно? Хотя я чувствую, что не сделал все связи ...

Правильно ли было бы, чтобы ad-hoc-полиморфизм удовлетворял (2), а параметрический полиморфизм удовлетворяет (3)? Но тогда как ad-hoc vs параметрически относится к разнице в RHS типов с семействами данных?

Одна последняя вещь, как бы суммировать значения типа, такие как

• Nothing :: forall a. Maybe a
• Right 3 :: forall a. Num b => Either a b

, когда они не имеют тип контекста вписывается в эту картину? Я предполагаю, что это пример (2)?

Answer 1

Условие индексированного по видам

В лямбда-кубе это параметрический полиморфизм.

В System F полиморфные термины выглядят как функции, которые принимают типы как аргументы и возвращают термины.

id : ∀ a. a -> a 
id = Λa . λx : a . x -- Λ binds type args, λ binds term args 

Они могут быть созданы путем явного применения их к типам:

boolId : Bool -> Bool 
boolId = id Bool 

В Haskell, язык пользовательского облицовочный не имеет явного применения типа и абстракции, так как определение типа может заполнить в детали в большинстве (но не во всех) случаях. Напротив, GHC Core, промежуточный язык для GHC Haskell, очень похож на систему F и имеет типовое приложение.

Тип стирания ортогонален тому, можно ли индексировать термины по типам. Это происходит так, что в Haskell типы могут быть удалены из среды выполнения, но мы могли бы представить другие языки, на которых не было объектов с равномерным размером времени выполнения, и, следовательно, им нужно было бы сохранять типы (или информацию о размере).

Типы индексированных по типам

В смысле лямбды-кубе это означает, имеющие функции от типов и конструкторов типов для типов и конструкторов типов.

Haskell не имеет аналогичной функции. Тип семьи приходят ближе, но они оба weaker and stronger.

типа классов и лямбда куб

классы типа странные звери, которые не смоделированные в лямбда-куба. В Haskell они отвлекаются на функции и перевод слов, поэтому они даже не появляются в GHC Core. Их можно рассматривать как некоторую предварительную обработку программ, которые полагаются на самонастраиваемую уникальность экземпляров, чтобы детерминистически заполнять детали.