Alexander Kuklev (akuklev) wrote,
Alexander Kuklev
akuklev

В обсчем, если ехать на Scala days, то вот с чем-то таким:

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

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)
Subscribe

  • (no subject)

    Встретил фотографию толпы футбольных фанатов, и она меня скорее напугала, у меня уж точно нет желания быть там среди них. Но внезапно я понял, что…

  • Прогресс

    Десять дней назад, вторая ступень SpaceX'овского корабля Starship своим ходом слетала своим ходом на десять километров вверх, и усмепшно приземлилась…

  • О водосбережении

    Как известно, питьевая вода во многих странах дефицитный ресурс. И даже в дождливой Германии летом иногда случаются засухи, в результате которых она…

  • Post a new comment

    Error

    default userpic

    Your reply will be screened

    Your IP address will be recorded 

    When you submit the form an invisible reCAPTCHA check will be performed.
    You must follow the Privacy Policy and Google Terms of use.
  • 4 comments