![[personal profile]](https://www.dreamwidth.org/img/silk/identity/user.png){kind=small}
codata, anybody can explain?
May. 22nd, 2013 02:53 pmhere the author hints we can have define fixed point of Succ. Well, it's Nat.
here Dan Piponi discusses in terms too obscure to me (yet) the aspects that kind of evade my comprehension.
here data and codata are defined simply as initial algebras and terminal coalgebras (over a comonad?)
It all looks logical but weird.
My practical gut feeling is that there's a BIG difference between potentially infinite data structures and strictly finite ones.
E.g. If I have a fully (c-like) structure, with no lists etc inside, I can successfully match it "in real time"; but if I have something that has a lazy list or whatever inside, it's impossible, and we actually have to work with it in a totally different way. Scan it, not match. With an exception of a map or a function, which we can ask for a value for a given key, without bothering with whatever else it contains.
There must be some pretty simple philosophy there, but somehow I cannot grasp it yet.
Update: Observational Type Theory may be the answer.
"Potentially more important than the formalisation of mathematical theories is the development of correct software for communicatin systems, which typically exhibit infinite behaviour and hence demand observational reasoning."
Practically, it may also tell us why we do not need DTD or type-safe JSON/REST.
here Dan Piponi discusses in terms too obscure to me (yet) the aspects that kind of evade my comprehension.
here data and codata are defined simply as initial algebras and terminal coalgebras (over a comonad?)
It all looks logical but weird.
My practical gut feeling is that there's a BIG difference between potentially infinite data structures and strictly finite ones.
E.g. If I have a fully (c-like) structure, with no lists etc inside, I can successfully match it "in real time"; but if I have something that has a lazy list or whatever inside, it's impossible, and we actually have to work with it in a totally different way. Scan it, not match. With an exception of a map or a function, which we can ask for a value for a given key, without bothering with whatever else it contains.
There must be some pretty simple philosophy there, but somehow I cannot grasp it yet.
Update: Observational Type Theory may be the answer.
"Potentially more important than the formalisation of mathematical theories is the development of correct software for communicatin systems, which typically exhibit infinite behaviour and hence demand observational reasoning."
Practically, it may also tell us why we do not need DTD or type-safe JSON/REST.
