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 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.
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]
On 11 April 2012 10:31, 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 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.
> 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]
> On 11 April 2012 10:31, 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 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.
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.
> On Wed, Apr 11, 2012 at 1:31 AM, Alexander Temerev <sor...@gmail.com > <mailto: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.
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.
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.
> 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 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.
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.
On Apr 12, 1:28 am, Tony Morris <tonymor...@gmail.com> wrote:
> 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.
> 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.
> > 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 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.
> 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.
> On Apr 12, 1:28 am, Tony Morris <tonymor...@gmail.com> wrote: > > 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.
> > 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.
> > > 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 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.
