The final version of our POPL paper on space-bounded FRP is available now -- we bought two extra pages from the ACM, and used them to add a lot more detail to the examples. With luck the paper will be a lot clearer now.
Also, Bob Atkey has a new blog post on using delay operators to model guarded definitions in type theory. He takes advantage of the fact that delay is a strong lax monoidal functor (with respect to the monoidal structure of products) to use the syntax of applicative functors.
This is a very elegant way of embedding these things into Haskell. Unfortunately, I have never liked the typing rules for the idiom syntax, since they don't work solely on the outermost type constructor. This means type-theoretic properties like normalization are messier to prove. (Bob evades this problem with semantic techniques, though.)
All his other posts are very good, too.
Also, Bob Atkey has a new blog post on using delay operators to model guarded definitions in type theory. He takes advantage of the fact that delay is a strong lax monoidal functor (with respect to the monoidal structure of products) to use the syntax of applicative functors.
This is a very elegant way of embedding these things into Haskell. Unfortunately, I have never liked the typing rules for the idiom syntax, since they don't work solely on the outermost type constructor. This means type-theoretic properties like normalization are messier to prove. (Bob evades this problem with semantic techniques, though.)
All his other posts are very good, too.
No comments:
Post a Comment