![[personal profile]](https://www.dreamwidth.org/img/silk/identity/user.png){kind=small}
(no subject)
Feb. 4th, 2012 03:54 amВ обсчем, если ехать на Scala days, то вот с чем-то таким:
1. Introduction
There is a quite convenient idiom (i.e. "abuse of notation") used throughout mathematics. Say, f: ℝ → ℝ is a real-valued function on the real line, and X ∈ ℝ is a set of real numbers. Notation f(X), which clearly does not typecheck, is intended to mean the image of X under action of f, i.e. X map f. In some context such idioms are highly desired.
We propose the notation for blocks with allowed idioms (to be called Idiom Brackets following McBride-Patterson'2008) which can be implemented in Scala mainly using macros with very few help from compiler: Whenever we have a polymorphic type F (like Set) which gives a rise to applicative functor (i.e. provides map and few other necessary constructions), we may write
implicit[F] { idiomatic_code }
where every usage of value of type F[Any] in idiomatic_code as an argument is interpreted as a map instead of apply, unless put into ‹literal brackets›.
As shown by McBride and Patterson, idiom brackets provide natural and concise syntax for a large class of calculations with side effects. For example, to incorporate logging into pure functions, one has to change the output type of each logged function from T to Logged[T], where Logged[T] contains the proper return value T together with accumulated logs. Composition of logged functions has to compose them on proper input and output values and concatenate logs. By using implicit[Logged] context, we can simply forget about it and work with Logged[A → B] functions as if they were pure A → B functions. Contexts like implicit[Volatile] and implicit[Throws] can provide clean syntax for some aspects of mutability and exception handling.
In the last section we discuss the possible generalization of idiom brackets for applicative arrow categories rather then (only applicative functors), which would allow reconsidering all imperative aspects of Scala to be result of the complete code being interpreted in implicit[Procedural] context.
* * *
Idiom brackets are essential for verifiable functions (aka constructive proofs). A verifiable function/constructive proof is a function returning a dependent Pair[r: T, P(r)] of an object (result) and proof that result sattisfies some desired condition P(r). In the implicit[VerifiableFunction]-context one would be able to compose verifiable functions as if they were returning only the result r: T and compose/concatenate propositions on the results automatically in background (analogously to implicit[Logging]).
For verifiable procedures one needs dependent tripples (Hoare tripples) instead of dependent pairs as described in Kleisli Arrows of Outrageous Fortune (McBride'2011) and the generalization of idiom brackets for applicative arrow categories would be required.
(To be continued)
Applicative contexts for Scala
1. Introduction
There is a quite convenient idiom (i.e. "abuse of notation") used throughout mathematics. Say, f: ℝ → ℝ is a real-valued function on the real line, and X ∈ ℝ is a set of real numbers. Notation f(X), which clearly does not typecheck, is intended to mean the image of X under action of f, i.e. X map f. In some context such idioms are highly desired.
We propose the notation for blocks with allowed idioms (to be called Idiom Brackets following McBride-Patterson'2008) which can be implemented in Scala mainly using macros with very few help from compiler: Whenever we have a polymorphic type F (like Set) which gives a rise to applicative functor (i.e. provides map and few other necessary constructions), we may write
where every usage of value of type F[Any] in idiomatic_code as an argument is interpreted as a map instead of apply, unless put into ‹literal brackets›.
As shown by McBride and Patterson, idiom brackets provide natural and concise syntax for a large class of calculations with side effects. For example, to incorporate logging into pure functions, one has to change the output type of each logged function from T to Logged[T], where Logged[T] contains the proper return value T together with accumulated logs. Composition of logged functions has to compose them on proper input and output values and concatenate logs. By using implicit[Logged] context, we can simply forget about it and work with Logged[A → B] functions as if they were pure A → B functions. Contexts like implicit[Volatile] and implicit[Throws] can provide clean syntax for some aspects of mutability and exception handling.
In the last section we discuss the possible generalization of idiom brackets for applicative arrow categories rather then (only applicative functors), which would allow reconsidering all imperative aspects of Scala to be result of the complete code being interpreted in implicit[Procedural] context.
Idiom brackets are essential for verifiable functions (aka constructive proofs). A verifiable function/constructive proof is a function returning a dependent Pair[r: T, P(r)] of an object (result) and proof that result sattisfies some desired condition P(r). In the implicit[VerifiableFunction]-context one would be able to compose verifiable functions as if they were returning only the result r: T and compose/concatenate propositions on the results automatically in background (analogously to implicit[Logging]).
For verifiable procedures one needs dependent tripples (Hoare tripples) instead of dependent pairs as described in Kleisli Arrows of Outrageous Fortune (McBride'2011) and the generalization of idiom brackets for applicative arrow categories would be required.
(To be continued)
