Я хочу определить списки, используя только определения этого типа:
data Unit = Unit
data Prod a b = P a b
data Sum a b = L a | R b
newtype Mu f = Mu (forall a . (f a -> a) -> a)
Мне удалось определить натуральные числа следующим образом:
zeroMu = Mu $ \f -> f $ L Unit
succMu (Mu g) = Mu $ \f -> f $ R $ g f
Я знаю, как определять списки с помощью дополнительного типа данных:
data ListF a x = NilF | ConsF a x
nilMu' = Mu $ \f -> f $ NilF
consMu' x (Mu g) = Mu $ \f -> f $ ConsF x $ g f
«Лучшее», что я могу получить, это это, но оно не проверяет тип (предполагаемый тип - µL.(1+(a*L))):
nilMu = Mu $ \f -> f $ L Unit
consMu x (Mu g) = Mu $ \f -> f $ R $ P x $ g f
Как я могу определить nilMu и consMu, используя только ранее определенные типы и их конструкторы?
Изменить
Как объясняет ответ @chi, это можно сделать, определив newtype следующим образом:
newtype F a x = F (Sum Unit (Prod a x))
nilMu = Mu $ \f -> f $ F $ L Unit
consMu x (Mu g) = Mu $ \f -> f $ F $ R $ P x $ g f
Он проверяет тип, но требует определения нового типа.
Цель этого вопроса состоит в том, чтобы расширить просто типизированную комбинаторную логику единицей, продуктом, суммой и рекурсивными типами. Первые три типа легко реализовать с помощью 7 новых комбинаторов (unit, pair, first, second, left, right, case). Рекурсивные типы также кажутся простыми в реализации, просто добавьте комбинатор конструктора типов mu, но, как показывает этот вопрос, он недостаточно гибок без дополнительных языковых конструкций.
Есть ли решение этой проблемы? Есть ли комбинаторная логика с рекурсивными типами для консультаций?
