Are haskell data types co
I'm trying to get my head around F-algebras, and this article does a pretty good job. I understand the notion of a dual in category theory, but I'm having a hard time understanding how F-coalgebras (the dual of F-algebras) relate to lazy data structures in Haskell.
F-algebras are described with an endofunctor with the function: F a -> a, which makes sense if you think of F a as an expression, and a as the result of evaluating that expression, as the linked article explains it.
Being the dual of F-algebras, the corresponding function for a F-coalgebra would be a -> F a. Wikipedia says that F-coalgebras can be used to create infinite, lazy data structures. How does the a -> F a functon allow one to create infinite, lazy data structures? Also, with that in mind, since Haskell is at it's core lazy, are most data-types in Haskell F-coalgebras instead of F-algebras? Are F-algebras not lazily evaluated?
If data types (or at least the ones that are capable of infinite data) are based on F-coalgebras in Haskell, what is the a -> F a function for lists, for example? What is the terminal F-coalgebra for lists?
Making an infinite list [1,2,3,4...] might look like this in Haskell:
list = 1 : map (+ 1) list
Does this use F-coalgebras somehow? Do infinite data structures require a notion of lazy evaluation and recursion alongside the use of F-coalgebras? Am I missing something here?
A coalgebra A -> FA can be used to peel away the outer layer of a (possibly infinite) data structure. For lists of X , the functor is F a = Maybe (X, a) , the same as in the algebraic view. In haskell the function for the coalgebra is
headView :: [a] -> Maybe (a, [a])
headView [] = Nothing
headView (x:xs) = Just (x,xs)
unfoldr is the unfold corresponding to this coalgebra, just like foldr is the fold corresponding to this algebra.
If you consider [a] not as the type of lists, but as a the type of descriptions of lists or programs, then this allows you to construct (seemingly) infinite values, just with a necessarily finite description.
As you can see, a Haskell list looks like both an F-algebra and an F-coalgebra. This is possible because Haskell is not actually consistent. You can fold an unfold, and get an infinite loop. Languages like coq and agda make the distinction between data types (F-algebras) and codata types (F-coalgebras) explicit. In those languages you have two list types, an algebraic List and a coalgebraic Colist .
上一篇: 在C中使用malloc为typedef'd类型分配空间
下一篇: Haskell数据类型co