(по мотивам языка 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 , [])". Достаточно удобно, но не совсем привычно. Совсем привычно не получается.

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