6 ms·
"Rich Hickey's transducers talk gave a nice example of how patterns of polymorphism which humans find comprehensible can easily become extremely hard to capture
by mej10 12y ago
"Rich Hickey's transducers talk gave a nice example of how patterns of polymorphism which humans find comprehensible can easily become extremely hard to capture precisely in a logic."
I haven't watched his talk, but Rich Hickey also commented on /r/Haskell with the types. It doesn't seem like it was that difficult to capture. There are also other comments that approach the types from different angles and achieve some success. Maybe this isn't a good example for this thesis?
http://www.reddit.com/r/haskell/comments/2cv6l4/clojures_transducers_are_perverse_lenses/cjjyay7 http://www.reddit.com/r/haskell/comments/2cv6l4/clojures_tra...
- swannodette 12y agoI don't think anything in that Reddit thread was conclusive, nor did they capture all of their properties (early termination, cleanup step).
- deleted 12y ago[deleted]
- bkirwi 12y agoYep, that's right. There seem to be a few factors involved: - Most of that discussion happened before a full description of transducers was up anywhere, so a lot of these details are just completely missing. - Haskell's type system is not expressive enough to capture certain interesting properties, like linearity. (To be clear, it's quite possible to translate any arbitrary transducer into Haskell -- but the type system will not prevent all the mistakes it is possible to make.) - There are different classes of transducers that Haskell people actively would not want to have identical types. (ie. stateful vs. stateless, early-terminating vs. unbounded) Many of the discussions revolve only one or a few of these classes -- typically the stateless unbounded version, which turns out to have a particularly simple encoding, but it definitely varies.
- tel 12y agoThose, I believe, are fairly easy to capture in the `Moore b r -> Moore a r` formulation. It also captures linearity. That said, I think the more general formulation is something like Fold or Traversal in Lens which operates polymorphically over the whole thing with a type that a refinement of Profunctor p => p a b -> p s t where such a type generalizes all of the concrete Haskell formulations.
- asolove 12y agoRich brought this up in his Strange Loop talk [1]. All the attempts he had seen either disallowed perfectly valid uses or allowed invalid ones. I believe to really guarantee early termination and a few other tricky invariants of reducers you would need a linear type system. [2] [1] https://www.youtube.com/watch?v=6mTbuzafcII https://www.youtube.com/watch?v=6mTbuzafcII [2] http://en.wikipedia.org/wiki/Substructural_type_system#Linear_type_systems http://en.wikipedia.org/wiki/Substructural_type_system#Linea...
- tome 12y agoWhat's wrong with allowing invalid ones? Surely transducers in an untyped language allow invalid ones too.
- icambron 12y agoTo the degree that it allows invalid types, it's weakly typed. That's fine as a compromise (no type system is perfect), but the same impulse that says you should type in the first place also says you should only allow valid types. It's a challenge type systems should aspire to solve.
- tome 12y agoThey should certainly aspire to solve it, but the inability to type one aspect of your program isn't an argument against types.
- icambron 12y agoThat you can't type it isn't an argument against types, but that you can't type it and that's perfectly fine with you suggests you don't actually think types are that important.
- eli_gottlieb 12y agoType systems do aspire to solve it, but we run into Rice's Theorem pretty quickly.