Я видел несколько вариантов использования полиморфизма ранга 2 (наиболее ярким примером является монада ST), но ни один для более высокого ранга, чем это. Кто-нибудь знает о таком варианте использования?
Пример использования полиморфизма ранга 3 (или выше)?
Ответы (2)
Возможно, я смогу помочь, хотя такой зверь неизбежно участвует. Вот шаблон, который я иногда использую при разработке синтаксиса с широким охватом с привязкой и индексированием де Брейна в бутылках.
mkRenSub ::
forall v t x y. -- variables represented by v, terms by t
(forall x. v x -> t x) -> -- how to embed variables into terms
(forall x. v x -> v (Maybe x)) -> -- how to shift variables
(forall i x y. -- for thingies, i, how to traverse terms...
(forall z. v z -> i z) -> -- how to make a thingy from a variable
(forall z. i z -> t z) -> -- how to make a term from a thingy
(forall z. i z -> i (Maybe z)) -> -- how to weaken a thingy
(v x -> i y) -> -- ...turning variables into thingies
t x -> t y) -> -- wherever they appear
((v x -> v y) -> t x -> t y, (v x -> t y) -> t x -> t y)
-- acquire renaming and substitution
mkRenSub var weak mangle = (ren, sub) where
ren = mangle id var weak -- take thingies to be vars to get renaming
sub = mangle var id (ren weak) -- take thingies to be terms to get substitution
Обычно я бы использовал классы типов, чтобы скрыть самое ужасное, но если вы распакуйте словари, вы найдете именно это.
Дело в том, что mangle
- это операция ранга 2, которая принимает понятие штуки, снабженной подходящими операциями, полиморфными в наборах переменных, над которыми они работают: операции, которые отображают переменные в штуки, превращаются в преобразователи терминов. Все это показывает, как использовать mangle
для генерации и переименования, и замены.
Вот конкретный пример этого шаблона:
data Id x = Id x
data Tm x
= Var (Id x)
| App (Tm x) (Tm x)
| Lam (Tm (Maybe x))
tmMangle :: forall i x y.
(forall z. Id z -> i z) ->
(forall z. i z -> Tm z) ->
(forall z. i z -> i (Maybe z)) ->
(Id x -> i y) -> Tm x -> Tm y
tmMangle v t w f (Var i) = t (f i)
tmMangle v t w f (App m n) = App (tmMangle v t w f m) (tmMangle v t w f n)
tmMangle v t w f (Lam m) = Lam (tmMangle v t w g m) where
g (Id Nothing) = v (Id Nothing)
g (Id (Just x)) = w (f (Id x))
subst :: (Id x -> Tm y) -> Tm x -> Tm y
subst = snd (mkRenSub Var (\ (Id x) -> Id (Just x)) tmMangle)
Мы реализуем термин обход только один раз, но в очень общем виде, затем мы получаем замену путем развертывания шаблона mkRenSub (который использует общий обход двумя разными способами).
В качестве другого примера рассмотрим полиморфные операции между операторами типов.
type (f :-> g) = forall x. f x -> g x
IMonad
(индексированная монада) - это некая m :: (* -> *) -> * -> *
, снабженная полиморфными операторами
ireturn :: forall p. p :-> m p
iextend :: forall p q. (p :-> m q) -> m p :-> m q
так что эти операции имеют ранг 2.
Теперь любая операция, параметризованная произвольной индексированной монадой, имеет ранг 3. Так, например, построение обычной монадической композиции,
compose :: forall m p q r. IMonad m => (q :-> m r) -> (p :-> m q) -> p :-> m r
compose qr pq = iextend qr . pq
полагается на количественную оценку 3-го ранга после того, как вы распаковываете определение IMonad
.
Мораль истории: как только вы занимаетесь программированием более высокого порядка над полиморфными / индексированными понятиями, ваши словари полезного набора получают ранг 2, а ваши общие программы - ранг 3. Это, конечно, эскалация, которая может произойти снова.
Возможно, лучший конец аннотации, которую я когда-либо читал: «Multiplate требует только полиморфизм 3-го ранга в дополнение к нормальному механизму классов типов в Haskell».. (О, только полиморфизм 3-го ранга, ничего страшного!)