Может ли компилятор Хаскеля сам генерировать instance Arbitrary для алгебраического типа?

Но ведь это же элементарно!

Делаешь пандорический захват, лифтишь в монаду, потом строишь рекурсивную схему (здесь подойдёт зигохистоморфный препроморфизм) как монадический трансформер из категории эндофункторов, и метациклически вычисляешь результат. Любой второкурсник справится. А если делать на анафорических лямбдах — так задачка вообще на пять минут.

Возможно ли это? Если да, то возможна ли чуть более сложная вещь - для части конструкторов определить генераторы вручную (у некоторых есть ограничения на множество значений аргументов), для остальных - автоматически?

И, кстати, данная процедура как-нибудь называется во всяких там теориях?

Например, стрелки. Единственный вариант, который я пока вижу. Нужно просто-типизированное LC это будет одна конструкция из стрелок/2-стрелок, нужно LC с зависимыми типами - другая, с субструктурными (линейными, в частности) - ещё третья. Т.е. фиксированное подмножество теории категорий само по себе довольно бедная метатеория, просто язык, в котором можно выразить все эти вещи. Мартин-Лёф предлагал формулировать разные теории типов в рамках метатеории LF, вот также это можно делать в рамках метатеории ТК.

Ну, например, берём декартово-замкнутую категорию Set, она же классический топос, т.е. категория всех малых множеств и тотальных функций, в agda она так и называется - «Set». Берём категорию всех малых категорий и функторов Cat (Set1 в agda) и утверждаем:

• Любой тип который может использоваться (ADTs, GADTs, Inductive families) это объект Set (объект топоса, в общем случае), т.е., как следствие, множество - множество всех термов данного типа.
• Любой параметрически-полиморфный тип это эндофунктор на Set, т.е. специального вида стрелка в Cat. (Непараметрический тип, который объект в Set, это вырожденный случай функтора из терминальной категории (как-то так)).
• Любой конструктор типа данных который может быть это стрелка в Set (стрелка в топосе, вообще).
• Любая функция которая может быть это тоже стрелка в Set, но отдельным классом (чтобы не путать стрелки-конструкторы и стрелки-функции). Как следствие, «функция» - тотальная функция между множествами.
• Любая композиция стрелок с учётом декартовых произведений и экспоненциалов это любой правильно составленный терм в данной системе (тут типизация из коробки).
• Любое определение конкретной редукции это 2-стрелка (струнная диаграмма).
• Любой конкретный ход редукций (вычислений) это композиции 2-стрелок (струнных диаграмм). + Правила построения редукций из коробки.

Например:

-- Тут рисуем коммутативную диаграмму:
ℕ : Set
0 : 1 → ℕ
s : ℕ → ℕ

-- Продолжаем коммутативную диаграмму:
+ : ℕ → (ℕ → ℕ)

-- Рисуем две струнных диаграммы, которые можно сочетать:
e₁(+) : + ∘ a ∘ 0 ⇒ a
e₂(+) : + ∘ a ∘ (s ∘ b) ⇒ s ∘ (+ ∘ a ∘ b)

и это просто ТК (можно представить формальный синтаксис такого языка), безотносительно какого-либо ЯП, но понятно из каких ADT и функции это получилось.

Тут ещё интересно, что можно легко добавлять конструкторы и правила редукций (как если бы в хаскеле можно было дописывать ADT и pattern matching cases по разным модулям).

Сами по себе 2-стрелки это непосредственно струнные диаграммы, т.е., рисуя коммутативные диаграммы, получим схемы типов, рисуя струнные - flow chart.

Второй анонимус круче первого. Haskell конечно штука необычная, но с ним гугл тоже помогает. Вот например вариант.

который содержит множество конструкторов, принимающих 0, 1 или 2 аргумента, для типов которых Arbitrary определен.

Проще всего это сделать с помощью Generics (в смысле не syb, а derive Generic).

Спасибо, что-то я забыл напрочь про Derive.

Автоматическая генерация instance'а с помощью него работает, замечательно. Но вот чтобы ограничить пространство значений стандартных типов придется делать новые типы с помощью newtype, я правильно понимаю?

Т.е. если у меня есть

data Command = Auth String | Read Int | Write String

newtype Login = Id String
newtype Id = Id Int
...
instance Arbitrary Login where
...
instance Arbitrary Id where
...
data Command = Auth Login | Read Id | ...

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

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