Я читаю о Lambda-Cube, и меня особенно интересует System F-omega, которая позволяет "операторам типа", то есть типам в зависимости от типов. Это очень похоже на семьи типа GHC. Например
type family Foo a
type instance Foo Int = Int
type instance Foo Float = ...
...
где фактический тип зависит от параметра типа a. Правильно ли я считаю, что семейства типов являются примером операторов типа ala F-omega? Или я в левом поле?
Система F-omega позволяет универсальную квантификацию, абстракцию и применение на более высоких видах, поэтому не только типы (в типе *), но также и в типах k1 -> k2, где k1 и k2 сами являются видами генерируется из * и ->. Следовательно, сам тип уровня становится просто типизированным лямбда-исчислением.
Haskell поставляет немного меньше, чем F-omega, поскольку система типов позволяет количественно и применять на более высоких видах, но не абстракции. Количественная оценка при более высоких видах - это то, как мы имеем такие типы, как
fmap :: forall f, s, t. Functor f => (s -> t) -> f s -> f t
с f :: * -> *. Соответственно, переменные типа f могут быть созданы с помощью выражений более высокого типа, например Either String. Отсутствие абстракции позволяет решать проблемы унификации выражений типов стандартными методами первого порядка, которые лежат в основе системы типа Хиндли-Милнера.
Тем не менее, типы семейств не являются действительно другим средством для введения более высокосортных типов, а также замены отсутствующего лямбда на уровне уровня. Реально они должны быть полностью применены. Итак, ваш пример,
type family Foo a
type instance Foo Int = Int
type instance Foo Float = ...
....
не следует рассматривать как введение некоторых
Foo :: * -> * -- this is not what happening
потому что Foo сам по себе не является значимым выражением типа. Мы имеем только более слабое правило: Foo t :: * всякий раз, когда t :: *.
Семейства типов, однако, действуют как отдельный механизм вычисления уровня на уровне F-omega, поскольку они вводят уравнения между выражениями типа. Расширение системы F с помощью уравнений - это то, что дает нам "Систему Fc", которую использует GHC сегодня. Уравнения s ~ t между выражениями типа вида * вызывают принуждения, переносящие значения от s до t. Вычисление производится путем выведения уравнений из правил, которые вы даете при определении семейств типов.
Кроме того, вы можете предоставить семействам типов более высокий тип возвращаемого типа, как в
type family Hoo a
type instance Hoo Int = Maybe
type instance Hoo Float = IO
...
так что Hoo t :: * -> * всякий раз, когда t :: *, но мы все же не можем оставить Hoo автономным.
Уловкой, которую мы иногда используем, чтобы обойти это ограничение, является newtype wrapping:
newtype Noo i = TheNoo {theNoo :: Foo i}
что действительно дает нам
Noo :: * -> *
но означает, что мы должны применить проекцию, чтобы сделать вычисление, поэтому Noo Int и Int являются предположительно различными типами, но
theNoo :: Noo Int -> Int
Итак, это немного неуклюже, но мы можем компенсировать тот факт, что семейства типов не соответствуют операторам типа в смысле F-омеги.