Purifying Scala
218 views
Skip to first unread message
Alexander Temerev
Apr 11, 2012, 4:31:11 AM4/11/12
to scala-debate
Me and Alexander Kuklev just presented our "Procedure Typing for
Scala" proposal. This is going to be at Scala Days (not in the general
track, unfortunately), but I also want to post it here. Comments are
welcome and highly appreciated.
The slides are here: http://www.slideshare.net/akuklev/scala-circuitries
Abstract:
The great attractiveness of purely functional languages is their
ability to depart from sequential order of computation. Theoretically,
it enables two important features of the compiler:
1) The ability to reorder computation flow, making the program
implicitly parallelisable. Modern imperative language compilers, even
using careful synchronization of concurrent code, still generate huge
chunks of sequential instructions that need to be executed on a single
processor core; a purely functional language compilers can dispatch
very small chunks to many (hundreds and thousands) of cores, carefully
eliminating as many execution path dependencies as possible.
2) As the compiler formalizes different types of side effects, it can
detect a whole new class of program errors at compile time, including
resource acquisition and releasing problems, concurrent access to
shared resources, many types of deadlocks etc. It is not yet a full-
fledged program verification, but it is a big step in that direction.
Scala is a semi-imperative language with strong support for functional
programming and rich type system. One can isolate the purely
functional core of the language which can be put on the firm
mathematical foundation of dependent type theories. We argue that it
is possible to treat Scala code as it’s written by now as an implicit
do-notation which can be then reduced to a purely functional core by
means of recently introduced Scala macros. The formalism of arrows and
applicative contexts can bring Scala to a full glory of an implicitly
parallelisable programming language, while still keeping its syntax
mostly unchanged.
Scala" proposal. This is going to be at Scala Days (not in the general
track, unfortunately), but I also want to post it here. Comments are
welcome and highly appreciated.
The slides are here: http://www.slideshare.net/akuklev/scala-circuitries
Abstract:
The great attractiveness of purely functional languages is their
ability to depart from sequential order of computation. Theoretically,
it enables two important features of the compiler:
1) The ability to reorder computation flow, making the program
implicitly parallelisable. Modern imperative language compilers, even
using careful synchronization of concurrent code, still generate huge
chunks of sequential instructions that need to be executed on a single
processor core; a purely functional language compilers can dispatch
very small chunks to many (hundreds and thousands) of cores, carefully
eliminating as many execution path dependencies as possible.
2) As the compiler formalizes different types of side effects, it can
detect a whole new class of program errors at compile time, including
resource acquisition and releasing problems, concurrent access to
shared resources, many types of deadlocks etc. It is not yet a full-
fledged program verification, but it is a big step in that direction.
Scala is a semi-imperative language with strong support for functional
programming and rich type system. One can isolate the purely
functional core of the language which can be put on the firm
mathematical foundation of dependent type theories. We argue that it
is possible to treat Scala code as it’s written by now as an implicit
do-notation which can be then reduced to a purely functional core by
means of recently introduced Scala macros. The formalism of arrows and
applicative contexts can bring Scala to a full glory of an implicitly
parallelisable programming language, while still keeping its syntax
mostly unchanged.
Eugene Burmako
Apr 11, 2012, 4:43:41 AM4/11/12
to Alexander Temerev, scala-debate
Really great job, guys!
I admire the fact that we can have your cake and eat it too. On the one hand, effects in this system are easily extensible (see slide 29), but on the other hand, they are transparent to the programmer (see slide 66) [slide numbers might become skewed, but for now they're okay]
Eugene Burmako
Apr 11, 2012, 4:54:36 AM4/11/12
to Alexander Temerev, scala-debate
Sorry, it should be slide 22 and slide 66
Alex Cruise
Apr 11, 2012, 1:49:53 PM4/11/12
to Alexander Temerev, scala-debate
On Wed, Apr 11, 2012 at 1:31 AM, Alexander Temerev <sor...@gmail.com> wrote:
Me and Alexander Kuklev just presented our "Procedure Typing for
Scala" proposal. This is going to be at Scala Days (not in the general
track, unfortunately), but I also want to post it here. Comments are
welcome and highly appreciated.
The slides are here: http://www.slideshare.net/akuklev/scala-circuitries
Quick note from the peanut gallery: I'm really excited about this. :)
Is there a paper, or even some code? :)
-0xe1a
HamsterofDeath
Apr 12, 2012, 1:36:07 AM4/12/12
to scala-...@googlegroups.com
where can i vote for this?
Tony Morris
Apr 11, 2012, 7:28:28 PM4/11/12
to scala-...@googlegroups.com
Hi Alexander,
I note you refer to a general category, then introduce a function
"affix" for parallelisability. I found it interesting that in Asymmetric
Lenses in Scala[1] section 5.1, I introduced the same morphism under the
name ***, since the lens category satisfies the affix operation too.
I note you refer to a general category, then introduce a function
"affix" for parallelisability. I found it interesting that in Asymmetric
Lenses in Scala[1] section 5.1, I introduced the same morphism under the
name ***, since the lens category satisfies the affix operation too.
Amusingly (in the context of lack of agreed naming), Russell O'Connor
and I, working on data-lens[2], had a some back-and-forth on how to name
this operation. We finally agreed on naming it Tensor.
[1] http://dropbox.tmorris.net/media/doc/lenses.pdf
[2] http://hackage.haskell.org/package/data-lens
> is possible to treat Scala code as it�s written by now as an implicit
> do-notation which can be then reduced to a purely functional core by
> means of recently introduced Scala macros. The formalism of arrows and
> applicative contexts can bring Scala to a full glory of an implicitly
> parallelisable programming language, while still keeping its syntax
> mostly unchanged.
--
Tony Morris
http://tmorris.net/
Alexander Temerev
Apr 12, 2012, 4:28:17 AM4/12/12
to scala-debate
The name "tensor" is certainly popular in this context among category
theorists, but we considered names more casual for software
developers / computer scientists (a monad is just a monoid in the
category of endofunctors, what's the problem, right?) That's why we
have chosen the name "circuitries" against somewhat more popular
"garrows". It is generally known that mathematicians suck at naming
things (groupoid, anyone?), so we had to be careful. Still, we
probably should be more deliberate in showing that what we propose is
just generalized arrows, as arrows (as a programming language
construct) are already widely known among Haskell developers and
theorists.
The other reason is that one category can often be equipped by several
different meaningful monoidal structures. The name "tensor product" is
customarily used for anything that works like the tensor product of
vector spaces and modules, i.e. for additive monoidal categories or
even pre-abelian ones.
> > is possible to treat Scala code as it s written by now as an implicit
theorists, but we considered names more casual for software
developers / computer scientists (a monad is just a monoid in the
category of endofunctors, what's the problem, right?) That's why we
have chosen the name "circuitries" against somewhat more popular
"garrows". It is generally known that mathematicians suck at naming
things (groupoid, anyone?), so we had to be careful. Still, we
probably should be more deliberate in showing that what we propose is
just generalized arrows, as arrows (as a programming language
construct) are already widely known among Haskell developers and
theorists.
The other reason is that one category can often be equipped by several
different meaningful monoidal structures. The name "tensor product" is
customarily used for anything that works like the tensor product of
vector spaces and modules, i.e. for additive monoidal categories or
even pre-abelian ones.
Tony Morris
Apr 12, 2012, 4:32:22 AM4/12/12
to Alexander Temerev, scala-debate
Well then, let's started the list of categories that are also circuitries.
* Any arrow (this list is immense)
* Lens
* Partial Lens
* Bijection
* Partial Bijection
Reply all
Reply to author
Forward
0 new messages