@Matthew,
I'm reading Conal's Compiling to Categories, and I've found some differences in how we represent functions in Language k.
For instance, we have:
neg :: h `k` Bool -> h `k` Bool
neg a = notC . a
But Conal, to represent functions has…
@Matthew,
Thanks !! I'll push all the code to the repository. If I have time today, I'll try to do some reading, because I'm getting behind with the papers.
@Matthew,
after taking away the functional dependencies, and changing the definitions of both adjunctions (catLeftAdjunct was missing a runKleisli) I have finally got:
instance Monad m => CatAdjunction (->) (Kleisli m) LeftK (RightK m) where…
@Matthew,
this is my take on the puzzles so far:
Puzzle1 solution: are the functor laws expressed in Category class terms:
catMap id = id
catMap (f . g) = catMap f . catMap g
Puzzle2 solution: is lifting returnand >=> from Monadto the Kl…
@Matthew,
the boilerplate code in
Kleisli puzzle finishes abrupty with
import Control.Monad ((, so I think there are some lines missing.
I've also needed to changeApplicative m to Monad m because it is needed for Keisli m to be a 'C…
@Matthew,
This restricts us from looking at one of the cutest adjunction constructions I know. If we have a Monad m, we compute two adjunctions! It's a classic construction. I don't think it's in Fong and Spivak It is at the heart of the >=&…
Hi @Matthew, here's my take on the puzzle:
I've created two classes, one for each preservation property
class PreservesCoproduct f where
extractCoproduct :: f (Either a b) -> Either (f a) (f b)
introduceCoproduct :: Either (f a) (f b) -&g…
@Matthew,
what a pull request !!! Most of the code was in need for a cleanup (mainly due to the fact that sometimes I was 'playing by ear', because my knowledge of Haskell is medium-plus at most).
I think that you're referring to "The simple esse…
@Anindya, Yes, but higher sometimes means "more abstract", that is, making less distinctions. In this interpretation, coarser (more abstract) is greater than finer (more concrete).
So I think both interpretations are valid and one has to choose the…
Hi Matthew,
The git repository is created at categories-working-hacker.
The last commit includes both your suggestions and an the modified interpreter.
I can enter in ghci the expression ex = lambda (lambda (add (before here) here)) only if I ena…
Matthew, after sleeping over my problem I think I've arrived at the solution of creating an intance of Interpret for the function (->) category which gets its Language instance from the general category one.
So, getting both run and interpretfor…
Hi Matthew, I've been working on your Puzzle3 and I'm stuck with the last twi pieces: run and interpret.
My code from Conal's paper is this:
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE FlexibleInstances #-}
…
@Matthew, I don't know if I have understood exactly what you meant with _|_, but my answer is this:
type Bottom = forall t. t
hilbertExplosion :: Bottom -> a
hilbertExplosion bottom = id bottom
Why is it called hilbertExplosion?
Matthew wrote
You skipped past puzzle #1 and answered #2!
I was suspecting that !! My fault was not to arrive to page 27 and feeling the right type for l ;-)
Consider flip (>>=) :: Monad m => (a -> m b) -> m a -> m b ...
…
@Matthew I've continued working with my puzzle about the relations between the proofs about adjunctions over posets in the book and implementations of the adjunctions in Haskell. Exercise 1.91 in the book asks us to prove, using Proposition 1.81, th…
Hi @Matthew, my take on Puzzle 1 is
instance Language (->) where
here (a, _) = a
before f (_, h) = f h
lambda f h a = f (a, h)
apply f g h = f h (g h)
loop f h = f h a where a = loop f h
int n _ = n
ad…
@Matthew I’ve arrived only at page 7 of Kiseliov’s notes. I’ll come back to the puzzle after finishing it.
The solution of my “puzzle” I suppose has to do with the second property of closure operators, because the second condition is just the join …
One relation between the haskell code for the Adjunction typeclass and the Galois connections in the text is, for example, the proof that \( p \le g(f(p)) \).
The proof starts with \( f(p) \le f(p) \), and then applies the adjunction to get \( p \l…
A good book alfter LYAH is Real World Haskell, which is also freely available at http://book.realworldhaskell.org/read/.
And the classic "reference" for typeclasses is the Typeclassopedia (https://wiki.haskell.org/Typeclassopedia) but it is very v…
And the last piece of Puzzle 4 is the State monad which can be "tested" with:
type MyState s = (((->) s) :.: ((,) s))
-- MyState s a = s -> (s, a)
inc = Comp1 (\s -> (s+1, s+1))
double = Comp1 (\s -> (s*2, s*2))
computation = do
…
Jim, I suppose that's because the first version I posted had extra spaces before the instances. Now I think the posted version is right. Haskell is very strict with indentation.
Tell me if there are more problems with the posted code and I'll try t…
After Mathew's suggestion (thanks !!), I've been able to finish all the code:
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE FunctionalDependencies #-}
{-# LANGUAGE Rank2Types #-}
{-# LANGUAGE TypeOperators #-…
In trying to solve Puzze 4, I'm having some compilation problems. When I define
instance Adjunction f g => Monad (g :.: f) where
return = Comp1 . unit
(>>=) = undefined
The compiler says it needs an Applicative for Monad (g :.: f…