Вариант использования для полиморфизма ранга 3 (или выше)? - PullRequest
Новая
       60

Вариант использования для полиморфизма ранга 3 (или выше)?

24 голосов
/ 06 декабря 2011

Я видел несколько вариантов использования для полиморфизма ранга 2 (наиболее ярким примером является монада ST ), но ни один из них не имел более высокого ранга. Кто-нибудь знает такой вариант использования?

Ответы [ 2 ]

30 голосов
/ 07 декабря 2011

Я могу быть в состоянии помочь, хотя такие звери неизбежно немного вовлечены. Вот схема, которую я иногда использую при разработке хорошо структурированного синтаксиса с привязкой и индексацией де Брюина, в бутылках. 

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. Это, конечно, эскалация, которая может произойти снова .

9 голосов
/ 07 декабря 2011
...