Как следует понимать общий тип функции «леммы»?

Question

Возможно, это глупый вопрос. Вот цитата из the Hasochism paper:

Одним из подходов к решению этой проблемы заключается в кодировании лемм, задаваемой параметризованных уравнений, как функция Haskell. В общем, такие Леммы могут быть закодированы как функции типа:

∀ x1 ... xn. Natty x1 → ... → Natty xn → ((l ~ r) ⇒ t) → t 

Я думал, что я понял RankNTypes, но я не могу разобраться в последней части этого предложения. Я читаю его неофициально как «заданный срок, который требует l ~ r, верните этот термин». Я уверен, что это толкование неверно, потому что это, по-видимому, приводит к округлости: мы не знаем l ~ r до завершения самого доказательства, поэтому как можно ожидать, что я должен представить в качестве предположения о доказательстве термин, который требует, чтобы ?

я ожидал бы равенство доказательства иметь тип больше, как это:

Natty x1 → ... → Natty xn → l :~: r 

неформально, «дал кучу Natty с, возвращающий доказательство того, что предложения l и r равны» (с использованием GHC Data.Type.Equality). Это имеет для меня гораздо больше смысла и, похоже, соответствует тому, что вы скажете в других системах с навязчивой системой. Я предполагаю, что это эквивалентно версии в газете, но я изо всех сил пытаюсь мысленно отделить две версии.

Одним словом, я смущен. Я чувствую, что мне не хватает ключевого понимания. Как читать тип ((l ~ r) => t) -> t?

Answer 1

Я читаю его как «данный термин, который требует l ~ r, возвращает этот термин»

Это «данный термин, тип которого содержит l, вернуть этот термин со всеми l s замещено по r с типа "(или в другом направлении r -> l). Это очень аккуратный трюк, который позволяет вам делегировать все cong, trans, subst и тому подобное в GHC.

Вот пример:

{-# LANGUAGE GADTs, DataKinds, PolyKinds, TypeFamilies, TypeOperators, RankNTypes #-} 

data Nat = Z | S Nat 

data Natty n where 
    Zy :: Natty Z 
    Sy :: Natty n -> Natty (S n) 

data Vec a n where 
    Nil :: Vec a Z 
    Cons :: a -> Vec a n -> Vec a (S n) 

type family (n :: Nat) :+ (m :: Nat) :: Nat where 
    Z  :+ m = m 
    (S n) :+ m = S (n :+ m) 

assoc :: Natty n -> Natty m -> Natty p -> (((n :+ m) :+ p) ~ (n :+ (m :+ p)) => t) -> t 
assoc Zy  my py t = t 
assoc (Sy ny) my py t = assoc ny my py t 

coerce :: Natty n -> Natty m -> Natty p -> Vec a ((n :+ m) :+ p) -> Vec a (n :+ (m :+ p)) 
coerce ny my py xs = assoc ny my py xs 

UPDATE

Поучительно специализироваться assoc:

assoc' :: Natty n -> Natty m -> Natty p -> 
      (((n :+ m) :+ p) ~ (n :+ (m :+ p)) => Vec a (n :+ (m :+ p))) 
               -> Vec a (n :+ (m :+ p)) 
assoc' Zy  my py t = t 
assoc' (Sy ny) my py t = assoc ny my py t 

coerce' :: Natty n -> Natty m -> Natty p -> Vec a ((n :+ m) :+ p) -> Vec a (n :+ (m :+ p)) 
coerce' ny my py xs = assoc' ny my py xs 

Daniel Wagner объяснил, что происходит в комментариях:

Или, говоря иначе, вы можете прочитать ((l ~ r) => t) -> t as, "заданный термин, который хорошо типизирован, предполагая, что l ~ r, возвращает тот же самый член из контекста, где мы доказали l ~ r, и разрядили его, что предположение ".

Давайте разработаем пробную часть.

В assoc' Zy my py t = t случае n равно Zy и, следовательно, мы имеем

((Zy :+ m) :+ p) ~ (Zy :+ (m :+ p)) 

, который сводится к

(m :+ p) ~ (m :+ p) 

Это явно идентичность и, следовательно, мы можем выполнить это предположение и вернуть t.

На каждом шаге рекурсии мы поддерживаем уравнение в

((n :+ m) :+ p) ~ (n :+ (m :+ p)) 

. Поэтому, когда assoc' (Sy ny) my py t = assoc ny my py t уравнение становится

((Sy n :+ m) :+ p) ~ (Sy n :+ (m :+ p)) 

, который сводится к

Sy ((n :+ m) :+ p) ~ Sy (n :+ (m :+ p)) 

в связи с определением (:+). А поскольку конструкторы инъективны

constructors_are_injective :: S n ~ S m => Vec a n -> Vec a m 
constructors_are_injective xs = xs 

уравнение становится

((n :+ m) :+ p) ~ (n :+ (m :+ p)) 

и мы можем назвать assoc' рекурсивно.

Наконец в вызове coerce' объединены эти два термина:

1. ((n :+ m) :+ p) ~ (n :+ (m :+ p)) => Vec a (n :+ (m :+ p)) 
2.          Vec a ((n :+ m) :+ p) 

Ясно Vec a ((n :+ m) :+ p) является Vec a (n :+ (m :+ p)) в предположении, что ((n :+ m) :+ p) ~ (n :+ (m :+ p)).

Answer 2

я ожидал бы равенство доказательства иметь тип больше, как это:

Natty x1 → ... → Natty xn → l :~: r 

Это разумная альтернатива. На самом деле, это логически эквивалентно одному в работе Hasochism:

{-# LANGUAGE GADTs, RankNTypes, TypeOperators, ScopedTypeVariables #-} 
module Hasochism where 

data l :~: r where 
    Refl :: l :~: l 

type Hasoc l r = forall t. (l ~ r => t) -> t 

lemma1 :: forall l r. Hasoc l r -> l :~: r 
lemma1 h = h Refl 

lemma2 :: forall l r. l :~: r -> Hasoc l r 
lemma2 Refl t = t 

В некотором смысле, Hasoc l r является непредикативным кодированием ограничения l ~ r.

Хазотистский вариант несколько проще в использовании, чем :~:, в том случае, если у вас есть, например,

type family A a 
-- ... 
proof1 :: Proxy a -> Hasoc a (A a) 
proof1 _ = -- ... 

вы можете просто использовать его как в

use1 :: forall a. [a] -> [A a] 
use1 t = proof1 (Proxy :: Proxy a) t 

Вместо этого, с

proof2 :: Proxy a -> a :~: A a 
proof2 _ = -- ... 

вы должны

use2 :: forall a. [a] -> [A a] 
use2 t = case proof2 (Proxy :: Proxy a) of Refl -> t 

Answer 3

У нас были прекрасные ответы, но как преступник, я думал, что уйду некоторые замечания.

Да, есть несколько эквивалентных представлений этих лемм. Презентация, которую я использую, является одной из них, и выбор во многом прагматичный. В эти дни (в более позднем кодовую), я иду так далеко, чтобы определить

-- Holds :: Constraint -> * 
type Holds c = forall t . (c => t) -> t 

Это пример типа выпрямитель: он абстрагирует над тем, что она обеспечивает (мотив элиминации) и он требует, чтобы вы построили ноль или более методов (один здесь) для достижения мотивов при более конкретных обстоятельствах. Способ читать это назад. Это говорит

Если у вас есть проблемы (населять любой тип мотива t), и никто не может помочь, может быть, вы можете достичь прогресса, если предположить, ограничение c в вашем методе.

Учитывая, что язык ограничений допускает конъюнкции (ака кортежей), мы получаем средства для написания лемм вида

lemma :: forall x1 .. xn. (p1[x1 .. xn],.. pm[x1 .. xn])  -- premises 
         => t1[x1 .. xn] -> .. tl[x1 .. xn]  -- targets 
         -> Holds (c1[x1 .. xn],.. ck[x1 .. xn]) -- conclusions 

и это может быть даже, что некоторые ограничения, помещение p или заключение c, имеет вид уравнения

l[x1 .. xn] ~ r[x1 .. cn] 

Теперь, чтобы развернуть такую ​​lemma, рассмотрит проблему наполнения отверстия

_ :: Problem 

Уточнить это _ устранением lemma, с указанием целей. Момент исходит из проблемы. Метод (единственное в случае Holds) остается открытым.

lemma target1 .. targetl $ _ 

и дырка метода не будут изменены типа

_ :: Problem 

но GHC будет знать кучу больше вещей, и, таким образом, более склонно верить ваше решение.

Иногда существует выбор ограничения по сравнению с данными для того, чтобы сделать предпосылку (ограничение) и цель (данные).Я предпочитаю выбирать их, чтобы избежать двусмысленности (Саймону нравится угадывать , но иногда ему нужен намек), а для облегчения доказательство по индукции, что намного проще по целям (часто это синглтоны для данных типа уровня), чем в помещениях.

Что касается развертывания, для уравнений, можно, конечно, переключиться на типе данных презентацию и вспыхивает анализ тематического

case dataLemma target1 .. targetl of Refl -> method 

и в самом деле, если вы вооружить себя с Dict экзистенциального

data Dict (c :: Constraint) :: * where 
    Dict :: c => Dict c 

вы можете сделать пучок сразу

case multiLemma blah blah blah of (Refl, Dict, Dict, Refl) -> method 

но форма выталкивателя более компактна и читаема , когда существует не более одного метода. Действительно, мы можем цепи несколько лемм без скольжения либо вправо

lemma1 .. $ 
... 
lemmaj .. $ 
method 

Если у вас есть такой выпрямитель с двумя или более случаев, я думаю, что это часто лучше, чтобы обернуть его как GADT, так что сайты использования услужливо маркировать каждый case с меткой конструктора.

Во всяком случае, да, дело в том, чтобы выбрать презентацию фактов, которые наиболее компактно позволяют нам расширить сферу применения механизмов решения ограничений ограничений GHC, чтобы больше вещей было просто typechecks. Если вы в отряде с Саймоном, это часто хорошая стратегия, чтобы объяснить себя Димитрию по соседству.