(Co)monads in ATS
199 views
Skip to first unread message
August Alm
Mar 16, 2017, 11:20:54 AM3/16/17
to ats-lang-users
Hi all!
I just wrote down some sketchy thoughts on monads and comonads in ATS. ATS has a very unique type system, so there are (co)monads in ATS that simply do not exist in other languages. I'm wondering if this might be useful. See the attached and let me know if you have ideas.
Best wishes,
August
I just wrote down some sketchy thoughts on monads and comonads in ATS. ATS has a very unique type system, so there are (co)monads in ATS that simply do not exist in other languages. I'm wondering if this might be useful. See the attached and let me know if you have ideas.
Best wishes,
August
Steinway Wu
Mar 17, 2017, 4:52:42 PM3/17/17
to ats-lang-users
Great note!
August Alm
Mar 17, 2017, 10:14:23 PM3/17/17
to ats-lang-users
Thank you!
I'll take this opportunity to expand on my note a bit. There are indeed several comonads in ATS generalizing the one I described. For example, one can construct:
vtypedef C(a: t0p) = [i: nat | i < n] [l: agz] (array_v(a, l, n), mfree_gc_v(l) | ptr(l))
Regard that as parametrizing arrays of type a (of fixed size n) with some choice of distinguished index i. There is an "extract" operation C(a) -> a that takes out
the i:th entry, and an "extend" operation
(C(a) -> b) -> (C(a) -> C(b))
that works as follows: An f: C(a) -> b reduces an array with a distinguished index to a term of b. Consider each index in turn as distinguished, to get n terms of b.
Then put those n elements into an array of size n of type b. Take the actual distinguished index as distinguished index of your new array. I haven't worked out the details
but it seems you can play similar games with most container types. What is sort of peculiar to me is that the "type part" in all cases is "ptr(l)", so almost all of the
comonadic abstractions are built on the view side of things, and the cost at runtime should be virtually nonexistent. I think it is certainly possible to do low-level programming
this way.
Comonads like the one described above are very useful. Consider image processing for example. Let the array be considered as a matrix, giving parameter values to the
pixels of a 2D image. There is often a recipe for transforming the parameters that depends on a pixel and its immediate neighbors, i.e. a function C(a) -> a. (A concrete
example is maybe a "blur" transformation, that takes a suitable average of the parameters of a pixel and that of its neighbors.) To transform the entire picture one would
"extend" to C(a) -> C(a). Conway's "Game of Life" is another example: Whether or not a cell survives to the next round depends on how crowded its immediate surrounding is.
Yet another example is parsing: You can't decide what to do with a single char without knowing its neighbors.
For a single transformation there is not so much gain in looking at things comonadically, but once you start composing several transformations of this form it can quickly get out
of hand without Kleisli composition to the rescue: since the effects depends on neighborhoods you can't change a point without changing how its neighbors will transform!
Programming in an imperative style with side effects side-steps the "need" for monads, but not for comonads. :)
My next ATS project will be to program an arduino-based effects pedal for electrical guitar. (I've seen people do that using C and there are many source code examples floating
around on the web.) Signal processing is another example of where comonads can be applied. (Say you measure a signal at discreet steps, but transform it based on neighboring
steps, so you have a contextual dependency.) I'm gonna give it a go!
PS. I think that in ATS it is best two imagine the types as forming not one category but two (or maybe three): type and viewtype. (Or t0ype and vt0ype.) The array construction
described above is perhaps most naturally regarded as a functor C: type -> viewtype. There is a sort of trivial inclusion J: type -> viewtype given by wrapping in a dataviewtype (so
datavtype J(a: type) = J of a) and one can regard C as a comonad relative to J.
I'll take this opportunity to expand on my note a bit. There are indeed several comonads in ATS generalizing the one I described. For example, one can construct:
vtypedef C(a: t0p) = [i: nat | i < n] [l: agz] (array_v(a, l, n), mfree_gc_v(l) | ptr(l))
Regard that as parametrizing arrays of type a (of fixed size n) with some choice of distinguished index i. There is an "extract" operation C(a) -> a that takes out
the i:th entry, and an "extend" operation
(C(a) -> b) -> (C(a) -> C(b))
that works as follows: An f: C(a) -> b reduces an array with a distinguished index to a term of b. Consider each index in turn as distinguished, to get n terms of b.
Then put those n elements into an array of size n of type b. Take the actual distinguished index as distinguished index of your new array. I haven't worked out the details
but it seems you can play similar games with most container types. What is sort of peculiar to me is that the "type part" in all cases is "ptr(l)", so almost all of the
comonadic abstractions are built on the view side of things, and the cost at runtime should be virtually nonexistent. I think it is certainly possible to do low-level programming
this way.
Comonads like the one described above are very useful. Consider image processing for example. Let the array be considered as a matrix, giving parameter values to the
pixels of a 2D image. There is often a recipe for transforming the parameters that depends on a pixel and its immediate neighbors, i.e. a function C(a) -> a. (A concrete
example is maybe a "blur" transformation, that takes a suitable average of the parameters of a pixel and that of its neighbors.) To transform the entire picture one would
"extend" to C(a) -> C(a). Conway's "Game of Life" is another example: Whether or not a cell survives to the next round depends on how crowded its immediate surrounding is.
Yet another example is parsing: You can't decide what to do with a single char without knowing its neighbors.
For a single transformation there is not so much gain in looking at things comonadically, but once you start composing several transformations of this form it can quickly get out
of hand without Kleisli composition to the rescue: since the effects depends on neighborhoods you can't change a point without changing how its neighbors will transform!
Programming in an imperative style with side effects side-steps the "need" for monads, but not for comonads. :)
My next ATS project will be to program an arduino-based effects pedal for electrical guitar. (I've seen people do that using C and there are many source code examples floating
around on the web.) Signal processing is another example of where comonads can be applied. (Say you measure a signal at discreet steps, but transform it based on neighboring
steps, so you have a contextual dependency.) I'm gonna give it a go!
PS. I think that in ATS it is best two imagine the types as forming not one category but two (or maybe three): type and viewtype. (Or t0ype and vt0ype.) The array construction
described above is perhaps most naturally regarded as a functor C: type -> viewtype. There is a sort of trivial inclusion J: type -> viewtype given by wrapping in a dataviewtype (so
datavtype J(a: type) = J of a) and one can regard C as a comonad relative to J.
Artyom Shalkhakov
Mar 18, 2017, 4:06:34 AM3/18/17
to ats-lang-users
Hi August,
On Thursday, March 16, 2017 at 9:20:54 PM UTC+6, August Alm wrote:
Hi all!
I just wrote down some sketchy thoughts on monads and comonads in ATS. ATS has a very unique type system, so there are (co)monads in ATS that simply do not exist in other languages. I'm wondering if this might be useful. See the attached and let me know if you have ideas.
Great note! I'm wondering if this observation can be used to drastically simplify some (view-)stateful functions? Consider this a challenge. :-) For instance, see this code:
It implements an imperative binary heap using linear types. Nearly every function follows the style: first, proofs are unpacked, then some useful work is done, and then proofs have to be packed back again. This is tiresome, as well as requires lots of fiddling around when re-factoring code. Can it be improved with comonads?
Best wishes,
August
gmhwxi
Mar 18, 2017, 8:27:07 AM3/18/17
to ats-lang-users
I really like the notes, too.
I would like to provide a bit of semantic background on viewtypes.
As the name suggests, a viewtype is just a view plus a type:
Semantically, one can always assume the following meta-property:
Given a viewtype VT, there exists a view V and a type T such that
VT = (V | T)
The linearity of a viewtype entirely comes from the linearity of the view
inside it.
I would like to provide a bit of semantic background on viewtypes.
As the name suggests, a viewtype is just a view plus a type:
Semantically, one can always assume the following meta-property:
Given a viewtype VT, there exists a view V and a type T such that
VT = (V | T)
The linearity of a viewtype entirely comes from the linearity of the view
inside it.
On Thursday, March 16, 2017 at 11:20:54 AM UTC-4, August Alm wrote:
gmhwxi
Mar 18, 2017, 8:35:18 AM3/18/17
to ats-lang-users
For a single transformation there is not so much gain in looking at things comonadically, but once you start composing several transformations of this form it can quickly get out
of hand without Kleisli composition to the rescue: since the effects depends on neighborhoods you can't change a point without changing how its neighbors will transform!
I completely agree.
This is why it is important to study category theory. At first, it seems
trivial but very soon one sees the power and the complexity of it. To
me (and many other people), Yoneda lemma is the first "impressive"
example.
For instance, you may want to take a look at the following interesting post:
http://www.haskellforall.com/2012/06/gadts.html
Cheers!
This is why it is important to study category theory. At first, it seems
trivial but very soon one sees the power and the complexity of it. To
me (and many other people), Yoneda lemma is the first "impressive"
example.
For instance, you may want to take a look at the following interesting post:
http://www.haskellforall.com/2012/06/gadts.html
Cheers!
gmhwxi
Mar 18, 2017, 8:48:48 AM3/18/17
to ats-lang-users
My next ATS project will be to program an arduino-based effects pedal for electrical guitar. (I've seen people do that using C and there are many source code examples floating
around on the web.) Signal processing is another example of where comonads can be applied. (Say you measure a signal at discreet steps, but transform it based on neighboring steps, so you have a contextual dependency.) I'm gonna give it a go!
I assume that you already know the following directory:
https://github.com/githwxi/ATS-Postiats-contrib/tree/master/contrib/arduino
which contains various short arduino examples. They all compile (I did check not
long ago).
As I see it now, the only downside of using ATS for an arduino project is that
template compilation may lead to bloated code size.
Hope that you will find a lot of fun and also inform us :)
Cheers!
On Friday, March 17, 2017 at 10:14:23 PM UTC-4, August Alm wrote:
gmhwxi
Mar 18, 2017, 12:20:46 PM3/18/17
to ats-lang-users
Maybe the GADT stuff (which I called GRDT in my original paper) is a bit
too involved. The G in GRDT stands for 'guarded', which I still think is a lot more
informative than the G in GADT, which stands for 'generalized'.
Even a simple maybe-monad is already pretty persuasive:
https://groups.google.com/forum/#!msg/ats-lang-users/qb0G4bivulk/BWy3li9T05UJ
Just imagine the effort needed to explicitly report an erroneous case to the top caller.
Anyone who implements parsing combinators can see this issue very clearly (though I
have to say that I myself prefer the exception-based solution here).
too involved. The G in GRDT stands for 'guarded', which I still think is a lot more
informative than the G in GADT, which stands for 'generalized'.
Even a simple maybe-monad is already pretty persuasive:
https://groups.google.com/forum/#!msg/ats-lang-users/qb0G4bivulk/BWy3li9T05UJ
Just imagine the effort needed to explicitly report an erroneous case to the top caller.
Anyone who implements parsing combinators can see this issue very clearly (though I
have to say that I myself prefer the exception-based solution here).
August Alm
Mar 18, 2017, 9:00:33 PM3/18/17
to ats-lang-users
I know T in VT = (V | T) can be gotten by the syntax VT?!. Is there an analogous syntax for extracting the view V
from VT ?
Also, I am unsure about how to think about this fact that all viewtypes are a product of a view and a type,
or more specifically, how it interacts with dependent types. How does it work in a simple case like
VT = [l: agz] (a@l | ptr(l)) ?
Clearly, VT is not ([l1: agz] a@l1 | [l2: agz] ptr(l2)). Is the existence of V merely existence or can it always be written
down constructively in the ATS syntax?
from VT ?
Also, I am unsure about how to think about this fact that all viewtypes are a product of a view and a type,
or more specifically, how it interacts with dependent types. How does it work in a simple case like
VT = [l: agz] (a@l | ptr(l)) ?
Clearly, VT is not ([l1: agz] a@l1 | [l2: agz] ptr(l2)). Is the existence of V merely existence or can it always be written
down constructively in the ATS syntax?
August Alm
Mar 18, 2017, 9:34:39 PM3/18/17
to ats-lang-users
Hi Artyom,
Cool code you got there. I don't think (co)monads per se are of much help that situation, but I do think that there might be some functoriality that could've shortened the code. I'll see what I can do. But generally, comonads are meant for functionally using data structures, not for defining them in the first place, so it was a tough challenge that you offered.
Btw, thanks for the link https://ashalkhakov.github.io/pats-ef/ (in another thread). I haven't used it much but just seeing stuff spelled out in tree-form like that made me better at reading the error messages myself.
Best wishes,
August
Cool code you got there. I don't think (co)monads per se are of much help that situation, but I do think that there might be some functoriality that could've shortened the code. I'll see what I can do. But generally, comonads are meant for functionally using data structures, not for defining them in the first place, so it was a tough challenge that you offered.
Btw, thanks for the link https://ashalkhakov.github.io/pats-ef/ (in another thread). I haven't used it much but just seeing stuff spelled out in tree-form like that made me better at reading the error messages myself.
Best wishes,
August
gmhwxi
Mar 18, 2017, 10:16:07 PM3/18/17
to ats-lang-users
Is the existence of V merely existence or can it always be written
down constructively in the ATS syntax?
It is merely existence.
What I should have written is this:
Semantically, a linear value vt can be thought of as a pair (v | t), where
v is a linear proof (of some view) and t is some data (non-linear value).
Of course, this is all intuition. It would require a huge effort to actually build
a model for only the core of ATS.
What I should have written is this:
Semantically, a linear value vt can be thought of as a pair (v | t), where
v is a linear proof (of some view) and t is some data (non-linear value).
Of course, this is all intuition. It would require a huge effort to actually build
a model for only the core of ATS.
August Alm
Mar 21, 2017, 9:28:30 AM3/21/17
to ats-lang-users
Is there a standard way to get the underlying [VT?!] part of a term [x: VT]?, i.e., some (polymorphic) function
VT -> VT?!
or
(&VT >> VT?!) -> void
?
VT -> VT?!
or
(&VT >> VT?!) -> void
?
Hongwei Xi
Mar 21, 2017, 9:41:48 AM3/21/17
to ats-lan...@googlegroups.com
--
You received this message because you are subscribed to the Google Groups "ats-lang-users" group.
To unsubscribe from this group and stop receiving emails from it, send an email to ats-lang-users+unsubscribe@googlegroups.com.
To post to this group, send email to ats-lang-users@googlegroups.com.
Visit this group at https://groups.google.com/group/ats-lang-users.
To view this discussion on the web visit https://groups.google.com/d/msgid/ats-lang-users/3cd0053d-e518-421e-9af1-c32c57240856%40googlegroups.com.
gmhwxi
Mar 21, 2017, 10:29:04 AM3/21/17
to ats-lang-users
But you could introduce a cast function (castfn):
castfn dataget{a:vt@ype}(x: !a): a?!
Actually, there is a dataget castfn in basics_dyn.sats:
https://github.com/githwxi/ATS-Postiats/blob/master/prelude/basics_dyn.sats
castfn dataget{a:vt@ype}(x: !a): a?!
Actually, there is a dataget castfn in basics_dyn.sats:
https://github.com/githwxi/ATS-Postiats/blob/master/prelude/basics_dyn.sats
On Tuesday, March 21, 2017 at 9:41:48 AM UTC-4, gmhwxi wrote:
No. This has to be done in an unsafe manner as the linear view part is discarded.
Reply all
Reply to author
Forward
0 new messages