Каково обоснование типа unoldr в Haskell?

Question

Пример, приведенный в документации unfoldr :: (b -> Maybe (a, b)) -> b -> [a]:

unfoldr (\b -> if b == 0 then Nothing else Just (b, b-1)) 10 

можно легко записать с резервированной пары:

unfoldr (\b -> if b == 1 then Nothing else Just (b-1, b-1)) 11 

Что unfoldr нужна пара (a,b) для? Почему его тип не (a -> Maybe a) -> a -> [a]?

Answer 1

Функция с типом

(a -> Maybe a) -> a -> [a] 

ограничивает выходной тип элемента списка, чтобы быть таким же, как состояние, которое резьбовое через процесс генерации. unfoldr более общий, поскольку он позволяет использовать независимый тип состояния.

Answer 2

Используя теорию, можно восстановить типы для сгибов/разворота рекурсивного типа, включая списки, понимая, почему они такие, какие они есть.

Да A быть фиксированным. «Список A S» типа удовлетворяет изоморфизм

List ~~ Either() (A, List) 

, который может быть прочитан «значение списка либо специальное значение (пустой список), или значение типа A следует значение списка».

В более емких обозначениях мы могли бы написать Either как инфикс +:

List ~~() + (A, List) 

Теперь, если мы позволим F b =() + (A, b), мы имеем, что приведенные выше

List ~~ F List 

является уравнением неподвижной точки, который всегда возникает при использовании рекурсивных типов.Для любого рекурсивного типа, определенного с помощью T ~~ F T мы можем вывести тип соответствующих складок/разворачивается (также известный как cata/ana или индукция/коиндукция принципы)

fold :: (F b -> b) -> T -> b 
unfold :: (b -> F b) -> b -> T 

В случае списков, тогда получит

fold :: ((() + (A, b)) -> b) -> List -> b 
unfoldr :: (b -> (() + (A, b))) -> b -> List 

разложенном также можно переписать отметить, что Maybe c ~~() + c:

unfoldr :: (b -> Maybe (A, b)) -> b -> List 

складка может вместо того, чтобы быть переписана с использованием

((x + y) -> z) ~~ (x -> z, y -> z) 

получение

foldr :: (() -> b, (A, b) -> b) -> List -> b 

затем, так как () -> b ~~ b,

foldr :: (b, (A, b) -> b) -> List -> b 

наконец, так как (x, y) -> z ~~ x -> y -> z (выделки), мы имеем

foldr :: b -> ((A, b) -> b) -> List -> b 

и снова:

foldr :: b -> (A -> b -> b) -> List -> b 

и с окончательным флип x -> y -> z ~~ y -> x -> z:

foldr :: (A -> b -> b) -> b -> List -> b 

---

Как эти типы следуют из (со) индукционных принципов?

теория домена гласит, что наименьшие неподвижные точки (F(T)=T) совпадают с приставкой мере точек (F(T)<=T), когда F монотонна в течение определенного посета.

Принцип индукции простой утверждает, что если T является наименьшей префиксовой точкой и F(U)<=U, то T<=U. (Proof. Это минимум!. Что и требовалось доказать.) В формулах

(F(U) <= U) ==> (T <= U) 

Чтобы справиться с неподвижными точками над типами, мы должны перейти от ч.у.м. к категориям, что делает все более сложным. Очень, очень грубо, каждый <= заменяется некоторым морфизмом. Например, F(U)<=U теперь означает, что существует некоторый морфизм F U -> U. «Monotonic F» означает, что F является функтором (начиная с a<=b, подразумевая, что F(a)<=F(b) теперь становится (a->b), подразумевая F a -> F b). Префиксными точками являются F-алгебры (F u -> u). «Наименее» становится «начальным». И так далее.

Следовательно, тип сгиба: (Подразумевается, -> а)

fold :: (F u -> u) -> (T -> u) 

Открывается вытекает из принципа коиндукции, который имеет дело с большими точками постфиксных T (которые становятся коалгебрами)

(U <= F(U)) ==> (U <= T)