Andy Melnikov (nponeccop) wrote,
Andy Melnikov
nponeccop

Category:

Зависимые типы и прологоподобные паттерны

vag_vagoff реализовал свой язык со статической типизацией, выводом типов и элементами зависимых типов. В частности, с типом Range - диапазоном целых чисел. В результате, например, + имеет такой тип (здесь и далее - псевдокод):

+ :: Range a b -> Range c d -> Range (a + c) (b + d), и в функцию, принимающую Range 0 10, можно передать значение типа Range 1 5, но нельзя передать значение типа Range 0 20.

Возникло желание прикрутить данный Range везде, где только можно, в частности, в условных конструкциях:
a :: Range 0 10
if (a >= 5)
{
    -- в этой ветке a имеет более узкий тип Range 5 10
}
else
{
    -- в этой ветке a имеет тип Range 0 10
}
В результате на ровном месте неявно имеем три разных a, что некрасиво. Сегодня утром мне пришла мысль синтаксически оформить это явно паттерн-матчингом:
data Nat = 0 | Succ a where
	a :: Nat

>= :: Range a Infinity -> a -> Nat where
	a :: Nat

pattern >= a 0
pattern >= (Succ a) (Succ b) :- >= a b
Здесь у меня используются неэффективные "унарные" натуральные числа, определяемые аксиомами Пеано. Похоже на нумералы Черча, но у меня Succ и 0 - конструкторы, а у Черча - обычные лямбда-выражения. Соответственно 2 - это Succ (Succ 0) и т д. Для простоты взял не конечный, а полубесконечный интервал. Infinity - это конструктор.

Как называть >=, я не определился. Предикат? Паттерн? Не делать отличия между такими паттернами и обычными АТД? Поэтому назвал его "паттерном". Используется >= например так:
f (>= x 5) = x + 2
f x = x + 3
что эквивалентно
f x
   | x >= 5 = x + 2
   | otherwise = x + 3
Но в первом случае, в отличие от второго, видно, что x разные: первый получается из второго "декомпозицией". При попытке матчинга эвалуатор работает похоже на унификатор в Прологе. Поэтому я не решился обозначить определение как = и использовал синтаксис :- Пролога. То есть, :- следует читать так: "для того чтобы проверить, попадает ли выражение >= x y под паттерн, проверьте, чтобы:

1) x попадал под паттерн Succ a
2) y попадал под паттерн Succ b
3) a и b попадали под паттерн >= a b

Можно было бы записать в форме, практически идентичной дизъюнктам Хорна, используемым в Прологе:
pattern >= x y :- x = Succ a, y = Succ b, >= a b
Но мне хотелось бы не путать a = b в значении "a редуцируется в b" и a = b в значении "a попадает под паттерн b", и одновременно не вводить новых операторов в духе a =~ b.
Tags: compiler design
Subscribe

  • Post a new comment

    Error

    default userpic

    Your reply will be screened

    Your IP address will be recorded 

    When you submit the form an invisible reCAPTCHA check will be performed.
    You must follow the Privacy Policy and Google Terms of use.
  • 2 comments