2 ms·

So, my primary confusion was on how to implement this in Haskell 2010 (without Rank[N,2]Types, GADTs, etc.), but I'd like to say I don't think we materially dis

by hawkice 12y ago

So, my primary confusion was on how to implement this in Haskell 2010 (without Rank[N,2]Types, GADTs, etc.), but I'd like to say I don't think we materially disagree about any matters of fact -- it isn't as though I'm pointing to code and claiming it shouldn't compile (as I'd seen the gist) or anything equally crazy. The specific polymorphism tradeoff I'm talking about would force the types to look a little more like... data Resumption [a, b, c...] where Resume :: x -> (x -> (a, Resumption [b, c, d...])) -> Resumption [a, b, c...] I think having dependent types means you could have something polymorphic with respect to the value :: [Type], which encompasses a large portion of what I'm pointing towards. This gets closer to covering the cyclic type system Rich Hickey mentioned, but I still think you'd have to be pretty careful to make sure the compiler doesn't explode with an infinite-sized type.

tel 12y ago
Ah, sorry, Haskell 2010 won't have nice enough types on its own. The best you could do would be to fake RankNTypes and use them for existentials. A sorrier state. You could definitely do something like what you ask. You could do something even nicer using a type family indexed on Nat. That all said, I don't know that I'm convinced that it's actually what was discussed in Hickey's slides even if his notation suggested it. You don't want your output changing at each step—you want the "sink" end of the applied transducer to pick the output and the "source" side to just treat it opaquely. Internal states stored local to a transduction "step" might be valuably treated as Rich suggests, but this is exactly what the Moore machine handles—the constructor can pick the state and the user can only pass it forward with some new variable each time they "open" the state. Furthermore, due to purity only one "sequence of reductions" can survive the whole process. This gives you your indexed types much more naturally. If you can think of a concrete use case where the more convoluted Nat-indexed type family would work better I'd be interested to see it. I'm reasonably convinced right now that it's closer to a sketch than a real need.

by hawkice 12y ago

tel 12y ago

Ah, sorry, Haskell 2010 won't have nice enough types on its own. The best you could do would be to fake RankNTypes and use them for existentials. A sorrier state. You could definitely do something like what you ask. You could do something even nicer using a type family indexed on Nat. That all said, I don't know that I'm convinced that it's actually what was discussed in Hickey's slides even if his notation suggested it. You don't want your output changing at each step—you want the "sink" end of the applied transducer to pick the output and the "source" side to just treat it opaquely. Internal states stored local to a transduction "step" might be valuably treated as Rich suggests, but this is exactly what the Moore machine handles—the constructor can pick the state and the user can only pass it forward with some new variable each time they "open" the state. Furthermore, due to purity only one "sequence of reductions" can survive the whole process. This gives you your indexed types much more naturally. If you can think of a concrete use case where the more convoluted Nat-indexed type family would work better I'd be interested to see it. I'm reasonably convinced right now that it's closer to a sketch than a real need.