March 10th, 2009

with Cat The Cat

Вопрос.

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

То есть, разрешены (по модулю завершимости):
data A : Set where
    A0 : A
    A1 : B -> A

data B : Set where
    B0 : B
    B1 : A -> B

f : ...
f = ... g ...

g : ...
g = ... f ...
А невозможно следующее:
data A : Set -> Set where
    A2 : (a : X) -> (b : f x) -> A Y

f : X -> Set
f ... = A Y
(опять же, условно)

В первых двух случаях понятно, что и как можно проверить.

В случае второго случая у меня, пока, взрывается мозг. Да и практического применения этому варианту я придумать не могу.