(по мотивам языка Agda2, примеры см. здесь, и Maude)

Mixfix синтаксис — когда положение аргументов функции или оператора задаётся специальными маркерами (Maude/Agda2 — подчеркиванием). Сами аргументы могут быть выражениями со своими правилами расположения аргументов и уровнями вложенности.

Примеры:
if_then_else_ — применять надо "if A then B else C"
_+_ — "1 + 2"
-_ — "- 10"

В сочетании с Юникодом получаются прикольные вещи. Да и без Юникода тоже ничего:

data [_] : A -> Set where
    [] : [ A ]
    _::_ : A -> [ A ] -> [ A ]

infixr 30 _||_
infix  20 _elem_

_elem_ : A -> [ A ] -> Bool
x elem [] = False
x elem (y :: ys) = x == y || x elem ys

-- BTW, elem__ отличается от _elem_

Так вот, в чём вопрос: что же можно описать с помощью mixfix синтаксиса?

В Maude можно даже списки описывать:

_,_ : A -> Q -> List
-- 1 , 2 , 3 будет списком.
-- кстати, упорядочение списка на Maude:
A , B => B , A if A < B -- это действительно так. ;)

Но Maude "слабо типизирован", это система переписывания термов, которая на этапе выполнения решает, принадлежит ли элемент множеству, или нет. То есть, он не ругнётся на "1 , 'a' , 3", а просто не сможет что-то выполнить.

А что можно описать в строго типизированном варианте?

Я попытался прикинуть, как и что надо задать, чтобы получить запись [[ 1 , 2 , 3 ]], чтобы писать списки практически удобным образом, но не смог понять, какой же тип должен быть у [_]].

Если переопределить "_,_ = _::_", то мы можем записывать списки так: "(1 , 2 , 3 , [])". Достаточно удобно, но не совсем привычно. Совсем привычно не получается.

Если у кого имеются (или появятся) мысли, милости прошу, очень интересно.

Здравствуйте, thesz, Вы писали:

T>Так вот, в чём вопрос: что же можно описать с помощью mixfix синтаксиса?

Ну вот тот же самый if then else например. case of, while do done, и прочие mixfix-конструкции.

T>Я попытался прикинуть, как и что надо задать, чтобы получить запись [[ 1 , 2 , 3 ]], чтобы писать списки практически удобным образом, но не смог понять, какой же тип должен быть у [_]].

T>Если переопределить "_,_ = _::_", то мы можем записывать списки так: "(1 , 2 , 3 , [])". Достаточно удобно, но не совсем привычно. Совсем привычно не получается.

T>Если у кого имеются (или появятся) мысли, милости прошу, очень интересно.

Все таки [1,2,3] -- это синтаксический сахар, переводимый в 1:2:3:[]. Как и [1..10] в enumFromTo. В Agda так, скорее всего, не выйдет. Можно поизголяться через universe-ы, в простых случаях, для фиксированного набора типов элементов получится.

Что-то в таком роде (синтаксис не помню, в agda не проверял)

data ListU : a -> Set where
  NatE : ListU Nat
  BoolE : ListU Bool
  ConsE : ListU a -> ListU a

list : ListU a -> Set
list NatE = Nat
list BoolE = Bool
list (ConsE a) = [a]

cons : hd -> {tl:ListU hd} -> (list tl) -> [hd]
cons hd {NatE} n = hd :: n :: []
cons hd {BoolE} b = hd :: b :: []
cons hd {ConsE} tl = hd :: tl

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

Можно чуть менее ограниченно решить в духе template metaprogramming с explicit specialization (или overlapping/еще какие-нить instances)

instance Cons a a where ...
instance Cons a [a] where ...

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

В общем можно сделать оператор _::_ который получая список ведет себя так, а примитив сяк. Но сделать его полиморфным в Agda, скорее всего, не выйдет. И будут проблемы, что 1::2 -- список, а 1 -- непонятно что. Можно еще с [_]] поизголяться, чтобы [[a :: b]] = a :: b и [a]] = a :: []. Но надо ли это.

T>>Так вот, в чём вопрос: что же можно описать с помощью mixfix синтаксиса?
V>Ну вот тот же самый if then else например. case of, while do done, и прочие mixfix-конструкции.

Получается многое, но не всё.

T>>Если у кого имеются (или появятся) мысли, милости прошу, очень интересно.
V>Все таки [1,2,3] -- это синтаксический сахар, переводимый в 1:2:3:[]. Как и [1..10] в enumFromTo. В Agda так, скорее всего, не выйдет. Можно поизголяться через universe-ы, в простых случаях, для фиксированного набора типов элементов получится.

Вот я и думал, а можно ли перевести синтаксический сахар в mixfix. Получается, что далеко не весь. Как минимум, без перегрузки не обойтись. Да и сравнение с образцом тоже будет страдать.

V>Но надо ли это.

"Мы отметём этот вопрос, как неорганизованный." (С) Выбегалло

У нас тут "фи-и-илосо-офия" программирования.

Здравствуйте, thesz, Вы писали:

T>>>Так вот, в чём вопрос: что же можно описать с помощью mixfix синтаксиса?
V>>Ну вот тот же самый if then else например. case of, while do done, и прочие mixfix-конструкции.

T>Получается многое, но не всё.

Ну так mixfix -- это все-таки infix + еще чуть-чуть. Некоторые формы на нем легко записываются, некоторые не очень. Полноценные синтаксические преобразования -- это уже дальше. В agda, думаю, есть более приоритетные задачи. Хотя может кто и сделает какие-нить hygienic mixfix macros

T>>>Если у кого имеются (или появятся) мысли, милости прошу, очень интересно.
V>>Все таки [1,2,3] -- это синтаксический сахар, переводимый в 1:2:3:[]. Как и [1..10] в enumFromTo. В Agda так, скорее всего, не выйдет. Можно поизголяться через universe-ы, в простых случаях, для фиксированного набора типов элементов получится.

T>Вот я и думал, а можно ли перевести синтаксический сахар в mixfix. Получается, что далеко не весь. Как минимум, без перегрузки не обойтись. Да и сравнение с образцом тоже будет страдать.

Оно и в хаскеле страдает. case [1..5] of [1..5] -> True; _ -> False. тоже не пашет ))

А по поводу [1,2,3] есть еще мысль сделать ф-ии _] _,_ и [_ -- может что и выйдет. Правда появится проблема с пустыми списками, и pattern match тоже не запашет. Но все-таки это не тот инструмент.

Здравствуйте, thesz, Вы писали:

T>Если у кого имеются (или появятся) мысли, милости прошу, очень интересно.
Надо просто вместо примитивного mixfix взять что-то поумнее. Например PEG.
Тогда можно будет описывать намного более широкий класс конструкций.
Ибо mixfix это подмножество регулярных грамматик, а PEG строго мощнее регулярных грамматик, почти полностью (*) покрывает контекстно свободные грамматики и захватывает часть контекстно зависимых.

* математически строгого описания взаимоотношений PEG и CFG насколько я знаю пока нет.

Короче если в Agda2 вместо (**) mixfix воткнуть PEG получится очень интересная штука. А если вспомнить про то что PEG может работать не только на основе текста но и принимать ЦУ от алгоритма вывода типов...

** можно и вместе ибо превратить mixfix в правило для PEG задача тривиальная

T>>Если у кого имеются (или появятся) мысли, милости прошу, очень интересно.
WH>Надо просто вместо примитивного mixfix взять что-то поумнее. Например PEG.
WH>Тогда можно будет описывать намного более широкий класс конструкций.
WH>Ибо mixfix это подмножество регулярных грамматик, а PEG строго мощнее регулярных грамматик, почти полностью (*) покрывает контекстно свободные грамматики и захватывает часть контекстно зависимых.

Ценно. Интересно.

Спасибо.

Здравствуйте, WolfHound, Вы писали:

WH>Здравствуйте, thesz, Вы писали:

T>>Если у кого имеются (или появятся) мысли, милости прошу, очень интересно.
WH>Надо просто вместо примитивного mixfix взять что-то поумнее. Например PEG.
WH>Тогда можно будет описывать намного более широкий класс конструкций.
WH>Ибо mixfix это подмножество регулярных грамматик, а PEG строго мощнее регулярных грамматик, почти полностью (*) покрывает контекстно свободные грамматики и захватывает часть контекстно зависимых.

Посмотрел чуть-чуть на PEG. Какой-то он очень низкоуровневый. В нем как-нибуть можно задавать приоритеты операций? И можно ли его вообще по человечески расширять?

Фишка infix/mixfix в том, что для расширения синтаксиса достаточно определить ф-ю и, возможно, добавить одну строку (ассоциативность с приоритетом) в том же модуле. Т.е. синтаксис расширяется модульно. Если для расширения синтаксиса понадобится лезть в парсер языка, то это не есть куль (если только у нас не лисп).

Можно ли, при помощи PEG, добавлять в язык правила по отдельности?

Здравствуйте, vshabanov, Вы писали:

V>Посмотрел чуть-чуть на PEG. Какой-то он очень низкоуровневый. В нем как-нибуть можно задавать приоритеты операций? И можно ли его вообще по человечески расширять?
Можно.
Также как и в CFG

<Expression> --> <Term> | <Term> + <Expression>
<Term>       --> <Factor> | <Factor> * <Term>
<Factor>     --> [ <Expression> ] | 0...9

Но так как правила будет добавлять парсер то никакой ручной возни с этой структурой не будет.

V>Фишка infix/mixfix в том, что для расширения синтаксиса достаточно определить ф-ю и, возможно, добавить одну строку (ассоциативность с приоритетом) в том же модуле. Т.е. синтаксис расширяется модульно. Если для расширения синтаксиса понадобится лезть в парсер языка, то это не есть куль (если только у нас не лисп).
Ну для того чтобы добавить конструкцию которую добавляет mixfix в парсер придется лезть не больше чем в случае с mixfix.
А там где mixfix'а маловато будет придется написать кусочек грамматики.
Но так mixfix в этом случае вообще ни на что не способен.
Например тот же конструктор списка будет выглядеть как-то так:

data Nat : Set where
  zero : Nat
  suc : Nat -> Nat

data Vec (A : Set) : Nat -> Set where
  [] : Vec A zero
  _::_ : {n : Nat} -> A -> Vec A n -> Vec A (suc n)

data List (A : Set) : Set where
  [] : List A
  _::_ : A -> List A -> List A

"[" list ("," list)* "]" : {A : Set}{n : Nat} -> (list : Vec A n) -> List A 
... list = vecToList list

Если компилятор в правиле находит несколько упоминаний одного значения и/или значение внутри оператора повторения то он засовывает все что разобрал в Vec A n где A тип значения, а n количество разобранных значений.

V>Можно ли, при помощи PEG, добавлять в язык правила по отдельности?
В том то и прелесть данного формализма что можно.
Более того правила можно добавлять по ходу разбора текста.
Те разобрал правило и сразу после этого оно может быть использовано.

Все руке не доходят прикрутить это дело к немерлу

WH>В том то и прелесть данного формализма что можно.
WH>Более того правила можно добавлять по ходу разбора текста.
WH>Те разобрал правило и сразу после этого оно может быть использовано.

С комбинаторами это получится хорошо. Видимые проблемы: рапорт об ошибках разбора и рапорт об ошибках проверки типов.

Здравствуйте, thesz, Вы писали:

WH>>В том то и прелесть данного формализма что можно.
WH>>Более того правила можно добавлять по ходу разбора текста.
WH>>Те разобрал правило и сразу после этого оно может быть использовано.
T>С комбинаторами это получится хорошо.
Вот тут я не понял как?
Ведь комбинаторный парсер это большое замыкание.
И я совершенно не понимаю как можно поменять потроха этого замыкания в процессе разбора теста этим замыканием.

T>Видимые проблемы: рапорт об ошибках разбора
Не хуже чем у любого рекурсивного парсера. А у них рапорты самые разборчивые.
Собственно PEG это и есть формальное описание рекурсивного парсера.

T>и рапорт об ошибках проверки типов.
Тут я вообще никаких проблем не вижу.

WH>>>В том то и прелесть данного формализма что можно.
WH>>>Более того правила можно добавлять по ходу разбора текста.
WH>>>Те разобрал правило и сразу после этого оно может быть использовано.
T>>С комбинаторами это получится хорошо.
WH>Вот тут я не понял как?
WH>Ведь комбинаторный парсер это большое замыкание.
WH>И я совершенно не понимаю как можно поменять потроха этого замыкания в процессе разбора теста этим замыканием.

pPEGDescr :: P (P Expr, P Pat)
pPEGDescr = ...

pFuncDef :: P Pat -> P Expr -> P FuncDef
pFuncDef pat expr = do
    funcName <- pIdent
    pats <- pMany pat
    pEqual
    expr <- pexpr
    return $ FuncDef funcName pats expr

pModule :: P Module
pModule = do
    pegs <- pMany parsePEGDescr
    let anyPattern = foldr combinePatDef defaultPatterns (map fst pegs)
    let anyExpression = foldr combineExpr defaultExpr (map snd pegs)
    funcs <- pMany (pFuncDef anyPattern anyExpression)
    return $ Module funcs

Плюс-минус, как-то так.

T>>Видимые проблемы: рапорт об ошибках разбора
WH>Не хуже чем у любого рекурсивного парсера. А у них рапорты самые разборчивые.
WH>Собственно PEG это и есть формальное описание рекурсивного парсера.

Да, тут будет умеренно просто. За исключением, возможно, если у нас получилось несколько вариантов разбора.

T>>и рапорт об ошибках проверки типов.
WH>Тут я вообще никаких проблем не вижу.

Мы сделали разбор образца и выражения, и они преобразуются во внутренние форматы. Все проверки идут над внутренними представлениями, поэтому и рапорт будет в их терминах, не в терминах использованных нами конструкций.

Здравствуйте, thesz, Вы писали:

T>Плюс-минус, как-то так.
Понятно. Только спроектировано криво.
Правила нужно тащить внутри монады, а не передавать явно.
В твоем случае создается куча ненужного шума, куча лишней работы если появятся еще группы правил, defaultPatterns и defaultExpr непонятного происхождения, все правила должны быть описаны вначале модуля, другие модули которые экспортируют правила тоже можно подключать только в начале, что ты будешь делать с конструкциями типа let open SomeModule in тоже не очень понятно,...

T>Да, тут будет умеренно просто. За исключением, возможно, если у нас получилось несколько вариантов разбора.
Тут нам может помочь типизатор. PEG по построению не имеет неоднозначностей. По этому будет выбрано первое правило которое позволило разобрать текст. Но если в процессе вывода типов возникла ошибка то мы можем откатиться и попробовать следующие правило.

T>Мы сделали разбор образца и выражения, и они преобразуются во внутренние форматы. Все проверки идут над внутренними представлениями, поэтому и рапорт будет в их терминах, не в терминах использованных нами конструкций.
Рапорт будет вида: В строке XXX по смещению YYY ожидается BlahMinor, а получен BlahMajor.
Если да то ИМХО проблем с пониманием в подавляющем большинстве случаев не будет.

T>>Плюс-минус, как-то так.
WH>Понятно. Только спроектировано криво.
WH>Правила нужно тащить внутри монады, а не передавать явно.
WH>В твоем случае создается куча ненужного шума, куча лишней работы если появятся еще группы правил, defaultPatterns и defaultExpr непонятного происхождения, все правила должны быть описаны вначале модуля, другие модули которые экспортируют правила тоже можно подключать только в начале, что ты будешь делать с конструкциями типа let open SomeModule in тоже не очень понятно,...

Запихивать вунтрь монады, или нет — вопрос второй.

Мне больше нравятся явно передаваемые параметры. Если уж они надоедают, тогда и вношу внутрь монады.

T>>Да, тут будет умеренно просто. За исключением, возможно, если у нас получилось несколько вариантов разбора.
WH>Тут нам может помочь типизатор. PEG по построению не имеет неоднозначностей. По этому будет выбрано первое правило которое позволило разобрать текст. Но если в процессе вывода типов возникла ошибка то мы можем откатиться и попробовать следующие правило.

Это означает наличие некоторого труда по организации всего этого дела.

T>>Мы сделали разбор образца и выражения, и они преобразуются во внутренние форматы. Все проверки идут над внутренними представлениями, поэтому и рапорт будет в их терминах, не в терминах использованных нами конструкций.
WH>Рапорт будет вида: В строке XXX по смещению YYY ожидается BlahMinor, а получен BlahMajor.
WH>Если да то ИМХО проблем с пониманием в подавляющем большинстве случаев не будет.

Он будет сложней, чем ты это представил, это точно.

Здравствуйте, thesz, Вы писали:

Думаю что можно сойтись на том что идея технически реализуема. Хоть и придется решить несколько непростых задач.
При этом получится система позволяющая описывать практически произвольный синтаксис.

Здравствуйте, WolfHound, Вы писали:

WH>Все руке не доходят прикрутить это дело к немерлу

Это дело сначала бы испытать.

Ты, кстати, куда пропал? 2 месяца ни слуха, ни духа.

Что до PEG, а то Packrat в чистом виде использовать нельзя.
Мыслей получилось довольно много, так что я изложил их в отдельном сообщении:
http://www.rsdn.ru/forum/philosophy/3403230.1.aspx

Автор: VladD2
Дата: 25.05.09

Здравствуйте, thesz, Вы писали:

T>Да, тут будет умеренно просто. За исключением, возможно, если у нас получилось несколько вариантов разбора.

Нескольких вариантов не может быть по определению. PEG их не допускает.
А соощения об ошибках можно сделать такими же разборчивыми как при написании парсера в ручную методом рекурсивного спуска. Собственно один и вариантов создания парсера по PEG — это создание рекурсивного нисходящего парсера с откатами.

T>>>и рапорт об ошибках проверки типов.
WH>>Тут я вообще никаких проблем не вижу.

T>Мы сделали разбор образца и выражения, и они преобразуются во внутренние форматы. Все проверки идут над внутренними представлениями, поэтому и рапорт будет в их терминах, не в терминах использованных нами конструкций.

Парсинг не имеет никакого отношения к семантичесому анализу. Как сделаешь так и будет. PEG позволяет вставлять тебе семантические предикаты. А то как ты их реализуешь — это твои проблемы.

T>>Мы сделали разбор образца и выражения, и они преобразуются во внутренние форматы. Все проверки идут над внутренними представлениями, поэтому и рапорт будет в их терминах, не в терминах использованных нами конструкций.
VD>Парсинг не имеет никакого отношения к семантичесому анализу. Как сделаешь так и будет. PEG позволяет вставлять тебе семантические предикаты. А то как ты их реализуешь — это твои проблемы.

Мне надо выдать сообщение об ошибке в терминах исходной программы, а не некоторого абстрактного ядра, куда всё транслируется.

Если у меня был список [1,2,3], то негоже будет его преобразовывать в (123:[]))), что сказать, что в нём ошибка.

Это мелочь, но очень удобно.

Здравствуйте, thesz, Вы писали:

T>Мне надо выдать сообщение об ошибке в терминах исходной программы, а не некоторого абстрактного ядра, куда всё транслируется.

T>Если у меня был список [1,2,3], то негоже будет его преобразовывать в (123:[]))), что сказать, что в нём ошибка.

T>Это мелочь, но очень удобно.

PEG это просто рекурсивный парсинг. Так, что еще раз повторю, как реализуешь так и будет. Тут проблемы точно искать не надо.

Проблемы будут в первую очередь в производительности.

T>>Мне надо выдать сообщение об ошибке в терминах исходной программы, а не некоторого абстрактного ядра, куда всё транслируется.
T>>Если у меня был список [1,2,3], то негоже будет его преобразовывать в (123:[]))), что сказать, что в нём ошибка.
T>>Это мелочь, но очень удобно.
VD>PEG это просто рекурсивный парсинг. Так, что еще раз повторю, как реализуешь так и будет. Тут проблемы точно искать не надо.

VD>Проблемы будут в первую очередь в производительности.

Ты меня не слушаешь.

Я не про разбор говорю, а про отображение обратно в исходный синтаксис для отчёта пользователю.

Здравствуйте, thesz, Вы писали:

T>Я не про разбор говорю, а про отображение обратно в исходный синтаксис для отчёта пользователю.
А не проще печатать исходную строку? — компиляторы обычно так и делают.