Hi @scolobb, thanks a lot for recommend me qi! qi is really excellent! I've read its document and lots of ideas come to me! I'd like to share them.
Start with the thoughts I experienced when I tried construct monad in
At first I noticed that a painter is essentially a side effect of drawing on a bitmap, and I wondered if I could convert it to a function that returns a bitmap. Inspired by Cartesian closed category, I realized that I needed an
apply function. With this
apply, I could regard painter as a mapping from frame to bitmap, which is composable (by
superpose) and there is an identity element of
blank (draw nothing)! Which means it's monoid! It drives me to construct monad.
Based on it, I defined
fmap, etc. and to my surprise, I thought I knew their semantics (even if I didn't prove that it's monad, I just tried to write them).
Map the transformation between frames to the transformation between bitmaps,
or map the procedure of drawing on a frame to the procedure of drawing directly on a bitmap.
- compose: superpose pictures together.
- return: blank picture.
- join: the picture drawn on a bitmap is also a bitmap.
- bind: like
apply-painter treats painter as a mapping from frame to bitmap,
bind treats painter as a mapping from bitmap to bitmap.
Proving "painter is monad" seems not to be so important -- we've defined these useful operator based on the idea.
Thinking back, in the original design of
sicp-pict, we regard picture as a process of drawing something with a frame. By this way, we only need to transform the frame to get the corresponding bitmap (similar to regard vector as the linear combination of bases in linear algebra).
We transform bitmap by transforming frame, but don't forget that we can transform bitmap directly! There must be some kind of connection between frame transformation and bitmap transformation! On the other hand, we can regard painter as a function that paints picture on a frame to get a bitmap. Can we let the painter paint directly on a bitmap? Wow, that's the
bind I defined at the beginning!
Here are some thoughts I got while studying category theory:
Can we move the abstraction and combinations in category theory to programming languages? If we can, to what category corresponding?
My answer to the 2nd question is that each type constructor (such as
Boxof) corresponds to a category, whose object is the
Values composed of the
Box type, and morphism is the mapping between these
We can construct 2 special type constructors, one of them is identity type constructor:
(define-type (Id A) A)
Id, we can regard any type
(Id A), which is an object in
Id category! And the type of any function not only can be regarded as a morphism between
Id, but also an endofunctor from
Another one is constant constructor (bitmap as an example):
(define-type (Bitmap) Frame)
(define-type (Bitmap A) (Instance Bitmap%))
And if we regard any constant
b with type
B as a function of type
(-> (Values 1) (Values B)) (marked
(-> 1 B)), which is an endofunctor in Id, then original morphism in Id (like f :
(-> B C)) become a natural transformation
(-> (-> 1 B) (-> 1 C)).
So that any value of
Frame can be regard as an endofunctor I = T^0 (mean no picture),
(Instance Bitmap%) can be regard as T(I) = T^1 (mean paint something in a frame T^0),
and T(T(I)) = T^2 (mean paint something in a bitmap T^1), etc.
Then we can define
η : I → T as blank (a painter that paint nothing on frame),
μ : T × T → T as identity (a bitmap painted something is also a bitmap), and they satisfy these laws:
μ ∘ Tμ = μ ∘ μT
μ ∘ Tη = μ ∘ ηT = 1
I'm not sure how category is used in purely functional language like Haskell, but I believe the essence of category theory is compose.
qi provides a very elegant and intuitive way to compose! I'd like to build typed qi too, but I suspect it's not that easy. In fact, I tried something and found that the existing type system has many restrictions on composition, see TR issues: 1172, 1175, 1176, 1218.
I think that the implementation of qi is based on the assumption that functions are mappings between
Values, but unfortunately TR's type system (and contract system) doesn't see it that way. TR has done a lot to the argument types in
-> rather than to
Values, thus it restricts the return types.
I plan to study how contract system works and try to define contract for values, and then based on it to improve
Values in TR, so that we can construct something like
(Values (Values Symbol String) *), which can be used as argument type or return type. And I guess
Values can also guide how to extend the Read and Write type in the future.