4 ms·
comonad encodes time, but first good paper i know of that describes this is 2006
by dustingetz 5y ago
comonad encodes time, but first good paper i know of that describes this is 2006
- ffhhj 5y agowhich paper?
- bradrn 5y agoWell, more generally speaking comonads encode costate i.e. context, but I haven’t yet seen them being used represent time. Do you have a link to the paper?
- dustingetz 5y agohttp://cs.ioc.ee/~tarmo/papers/essence.pdf http://cs.ioc.ee/~tarmo/papers/essence.pdf also it needs to be updated for cofree comonad
- bradrn 5y agoThank you!
- mumblemumble 5y agoWell, the interview never really addresses this clearly and directly, but my sense was that it seemed that the biggest problem he was grappling with was dealing with situations where things have to happen in a certain order. The formulation of functional programming that he presented in Can Programming be Liberated from the Von Neumann Style? is, at least to my reading, pure and lazy. For a while at least, nobody really knew how to deal with things where time matters in even the most basic way - ensuring that they happen in a certain order, or even at all - in a pure and lazy language. The Haskell community figured out how to use monads to crack that problem in the early 1990s. Haskell 1.0 didn't have monadic IO, what it had instead was, from what I've read, kind of an unwieldy hack. SPJ covers these sorts of issues in some detail in his paper Tackling the Awkward Squad: https://www.microsoft.com/en-us/research/publication/tackling-awkward-squad-monadic-inputoutput-concurrency-exceptions-foreign-language-calls-haskell/ https://www.microsoft.com/en-us/research/publication/tacklin...
- ulrikrasmussen 5y agoDid Clean have uniqueness typing from it's inception ('87)? That's another way to deal with time.
- edflsafoiewq 5y agoIO solves the "time problem" by just encoding a von Neumann machine in the functional language, which is less like a liberation than a peace treaty.
- creata 5y agoMaybe my imagination is too small, but what else could a solution look like? You want sequencing, and IO gives you exactly that.
- dustingetz 5y agostream, signal, and differential programming
- mumblemumble 5y agoPerhaps. But I think that you're also wandering away from the plot. Clinging to our contemporary way of thinking about this stuff isn't really going to help us understand what he was grappling with 30, 40 years ago. It's more likely to muddy the waters. I don't see any evidence in there that Backus was looking for anything quite so lofty as the stuff you're bringing up. While it's true he wrote the paper that kicked off the whole idea behind FP, we've also got to keep in mind that, as he repeatedly mentions in the interview, he was a lifelong Fortran programmer who, in marked contrast to most fans of FP nowadays, held a lifelong affinity for Fortran. It sounds to me like encoding Von Neumann bits into the functional language so that you're there when you need them is exactly the sort of thing he was looking for. To my reading, his Turing lecture would seem to suggest the same.
- juliangamble 5y agoCould you provide a link or example?
- catgary 5y agoI feel like Hagino had talked about coinductive data types in the early 90’s.