Здравствуйте, 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 :: []. Но надо ли это.