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]](../../../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]](../../../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.
