Log in

No account? Create an account


Recent Entries




June 9th, 2019


Языки программирования от Фортрана и Кобола до Caml и Java играют ключевую роль в управлении сложными компьютерными системами. Книга «Введение в теорию языков программирования» представляет читателю средства, необходимые для проектирования и реализации подобных языков. В ней предлагается единый подход к различным формализмам для определения языков программирования – операционной и денотационной семантике. Особое внимание при этом уделяется способам задания отношений между тремя объектами: программой, входным значением и результатом. Эти формализмы демонстрируются на примере таких типичных элементов языков программирования, как функции, рекурсия, присваивание, записи и объекты. При этом показывается, что теория языков программирования состоит не в последовательном изучении самих языков один за другим, а строится вокруг механизмов, входящих в различные языки. Изучение таких механизмов в книге приводит к разработке вычислителей, интерпретаторов и компиляторов, а также к реализации алгоритмов вывода типов для учебных языков.

June 2nd, 2019

Лёд тронулся

по мотивам https://xacid.dreamwidth.org/70479.html где я недоумевал по поводу отсутсвия в дотти синт-сахара для полиморфных лямбд и вобще функций первого класса - кажется до них таки это доперло


теперь в дотти будут (уже замержили в мастер) такие полиморфные лямбды

// Polymorphic idenity
val pid = [T] => (t: T) => t

// Function with poly function argument
val mf = (f: [U] => U => U, t: Int) => f(t)
val mf0 = mf(pid, 23)

May 25th, 2019

CPS-translation as adjoint


CPS-translation as adjoint

We show that there exist translations between polymorphic \-calculus and a subsystem of minimal logic with existential types, which form a Galois insertion (embedding). The translation from polymorphic -calculus into the existential type system is the so-called call-by-name CPS-translation that can be expounded as an adjoint from the neat connection. The construction of an inverse translation is investigated from a viewpoint of residuated mappings. The duality appears not only in the reduction relations but also in the proof structures, such as paths between the source and the target calculi. From a programming point of view, this result means that abstract data types can interpret polymorphic functions under the CPS-translation. We may regard abstract data types as a dual notion of polymorphic functions.

May 14th, 2019


In this paper, we take a fresh look at automatic differentiation (AD) techniques, and especially aim to demystify the reverse-mode form of AD that generalizes back-propagation in neural networks.We uncover a tight connection between reverse-mode AD and delimited continuations, which permits implementing reverse-mode AD purely via operator overloading and with-out managing any auxiliary data structures.

April 10th, 2019


Faster Coroutine Pipelines:A Reconstruction (Extended Version)

Ruben P. Pieters, Tom Schrijvers
Report CW 715, November 2018
Department of Computer Science, KU Leuven

Spivey has recently presented a novel functional representation that supports the efficient composition, or merging, of coroutine pipelines for processing streams of data. This representation was inspired by Shivers and Might’s three-continuation approach and is shown to be equivalent to a simple yet inefficient executable specification. Unfortunately, neither Shivers and Might’s original work nor the equivalence proof sheds much light on the underlying principles allowing the derivation of this efficient representation from its specification.This paper gives the missing insight by reconstructing a systematic derivation in terms of known transformation steps from the simple specification to the efficient representation. This derivation sheds light on the limitations of the representation and on its applicability to other settings. In particular, it has enabled us to obtain a similar representation for pipes featuring two-way communication,similar to the Haskell pipes library. Our benchmarks confirm that this two-way representation retains the same improved performance characteristics

Faster coroutine pipelines


Faster coroutine pipelines

Michael Spivey University of Oxford, UK, 2017

Coroutine pipelines provide an attractive structuring mechanism for complex programs that process streams of data, with the advantage over lazy streams that both ends of a pipeline may interact with the I/O system, as may processes in the middle. Two popular Haskell libraries, Pipes and Conduit, support such pipelines. In both libraries, pipelines are implemented in a direct style by combining a free monad of communication events with an interpreter for (pseudo-)parallel composition that interleaves the events of its argument processes. These implementations both suffer from a slow-down when processes are deeply nested in sequence or in parallel. We propose an alternative implementation of pipelines based on continuations that does not suffer from this slow-down. What is more, the implementation is significantly faster on small, communication-intensive examples even where they do not suffer from the slow-down, and comparable in speed with similar programs based on lazy streams. We also show that the continuation-based implementation may be derived from the direct-style implementation by algebraic reasoning.

April 9th, 2019

Coroutine pipes


object Pipes {

  sealed trait Pipe[I, O, R] {

    final def flatMap[T](f: R => Pipe[I, O, T]): Pipe[I, O, T] = this match {
      case Yield(b, p) => Yield(b, () => p() flatMap f)
      case Await(k) => Await(a => k(a) flatMap f)
      case Ready(r) => f(r)
Read more...Collapse )

February 25th, 2019

Continuation recursion


  import IxCont._

  println(unfold(10)(_ + 1).take(10).toList)

    def nat(n: Int) = loop(for {
      x <- take[Int, Stream[Int]]
      _ <- put(x)
    } yield x + 1)(n)


    def nat(n: Int) = loop(for {
      x <- channel[Int, Int]
      _ = println("x:" + x)
    } yield x + 1)(n) toStream


    def f = loop(for {
      x <- take[Int, String @@ Int]
      _ = println("x = " + x)
      y <- suspend[Int, String](s"[$x]")
      _ = println("y = " + y)
    } yield x + y)


Read more...Collapse )
Powered by LiveJournal.com