Thu 9 Nov 2006
If we take a look at the Haskell (.) operator:
(.) :: (a -> b) -> (e -> a) -> e -> b
and take a moment to reflect on the type of fmap
fmap :: Functor f => (a -> b) -> f a -> f b
and the unnamed Reader monad from Control.Monad.Reader
instance Functor ((->) r)
we see that fmap applied to the Reader functor rederives (.).
Thu 9 Nov 2006
A number of us from the freenode #haskell channel have gone and formed/revived ##logic to avoid overwhelming the main Haskell channel with traffic. Originally, I just wanted to revive the #logic channel that was already there, but upon talking to the freenode staff, it appears that they have channel naming guidelines that preclude topical discussion channels getting single # names without some sort of clear trademark. They were however nice enough to forward the previous #logic channel to the new location.
In any event, if you are interested in logic at pretty much any level, feel free to stop by the channel.
Wed 1 Nov 2006
Was reading Castagna, Ghelli, and Longo's 1995 paper on "A Calculus for Overloaded Functions with Subtyping" today and in it they have to jump through some hoops to index their '&' types to keep them well behaved under β-reduction.
It seems to me, at least from my back-of-the-envelope scribblings, that if you CPS transform the calculus before, that the main technical innovation (overloaded functions using the tighter run-time type information) remains intact, but the need for this technical trick goes away. In this case you know what the reduction will evaluate out to regardless of call-by-value or call-by-need (just bottom), and if the specification changes during evaluation it is still sound, so no need for an index.
![\inference{\Gamma \vdash M:W_1 \leq \lbrace\neg U_i\rbrace_{i\leq(n-1)} & \Gamma \vdash N : W_2 \leq \neg U_n}{\Gamma \vdash (M \binampersand N) : \lbrace \neg U_i \rbrace_{i \leq n }}[$\lbrace\rbrace$-I]](http://comonad.com/latex/63ee3379bf761ad7074f3bb895da57d5.png "\inference{\Gamma \vdash M:W_1 \leq \lbrace\neg U_i\rbrace_{i\leq(n-1)} & \Gamma \vdash N : W_2 \leq \neg U_n}{\Gamma \vdash (M \binampersand N) : \lbrace \neg U_i \rbrace_{i \leq n }}[$\lbrace\rbrace$-I]")
![\inference{\Gamma \vdash M : \lbrace \neg U_i \rbrace_{i \in I} & \Gamma \vdash N : U & U_j = \min_{i \in I} \lbrace U_i \vert U \leq U_i \rbrace } {\Gamma \vdash M \bullet N : \perp }[$\lbrace\rbrace$-E]](http://comonad.com/latex/b5ad9c35b4aeb655526d34f61cc0b770.png "\inference{\Gamma \vdash M : \lbrace \neg U_i \rbrace_{i \in I} & \Gamma \vdash N : U & U_j = \min_{i \in I} \lbrace U_i \vert U \leq U_i \rbrace } {\Gamma \vdash M \bullet N : \perp }[$\lbrace\rbrace$-E]")
The above then would requires explicit continuations and might interfere with rederiving tupling from the overloading mechanism alone, but seems to eliminate some of the barriers they mention to the higher order case. However, I'm not convinced it is a net win regardless, because it would require a notion of typecase.
Thu 26 Oct 2006
I almost have the blog integrated with the old slipwave wiki content. I kludged something together to display it in WordPress. While I may add a flashy dynamic in-page loading feature like TiddlyWiki, for right now its functional and backwards compatible with my old content and gracefully degrades in the absence of javascript.
By way of example, you might try to view some Haskell source code.
This also might provide better context when I start to talk about things like continuations because I can link right inline to more extended static content.
This also provides me with a more convenient venue for static content than WordPress' default page management system.
Please, let me know if some bit of markup doesn't show up right.
Tue 17 Oct 2006
import qualified Control.Comonad as Comonad import qualified Edward hiding (personal_details) import Blog.Software -- Hello, World! instance Blog Comonad.Reader where url = "http://comonad.com/reader" author = Edward.Kmett main = forever $ post stuff
Syntax highlighting works.
![\inference{}{\Gamma, x:\tau \vdash x:\tau}[var]](http://comonad.com/latex/e645c5ec70f37ece72dd6cfe28d4f4e6.png "\inference{}{\Gamma, x:\tau \vdash x:\tau}[var]")
![\inference{\Gamma,x:\sigma \vdash M:\tau}{\Gamma \vdash \lambda x : \sigma. M : \sigma \rightarrow \tau}[abs]](http://comonad.com/latex/05f05269088d58a918791c0832838cb5.png "\inference{\Gamma,x:\sigma \vdash M:\tau}{\Gamma \vdash \lambda x : \sigma. M : \sigma \rightarrow \tau}[abs]")
![\inference{\Gamma \vdash M : \sigma \rightarrow \tau & \Gamma \vdash N:\sigma}{\Gamma \vdash M N : \tau}[app]](http://comonad.com/latex/6b489a895eb7d0e43a552fdda5bd3a6a.png "\inference{\Gamma \vdash M : \sigma \rightarrow \tau & \Gamma \vdash N:\sigma}{\Gamma \vdash M N : \tau}[app]")
Apparently, 
works.
![\bfig \square/>>`>`>` >->/[A`B`C`D;e`f`g`m] \morphism(500,500)|m|/.>/< -500,-500>[B`C;h] \efig](http://comonad.com/latex/4fd5bd37f2fbd56aafb426d35dafa6d9.png "\bfig \square/>>`>`>` >->/[A`B`C`D;e`f`g`m] \morphism(500,500)|m|/.>/< -500,-500>[B`C;h] \efig")
Commutative diagrams, check.
All systems go.
World, meet blog; blog, meet world.
