Journal de Chaource

Groovy used to be a niche scripting language, not of concern to anyone, until it got into Hudson, which was then forked as Jenkins. Everybody today uses Jenkins and so everybody is forced to use Groovy. What a mad world.

What does this code do?

 parallel(
    "job1" : {
        url = "http://host1/file1"
        sh "curl -o file1 ${url}"
    },
    "job2" : {
        url = "http://host2/file2"
        sh "curl -o file2 ${url}"
    }
)

At first glance, you'd think it downloads two URLs in parallel and saves them to files "file1" and "file2".

But actually the variable "url" is global. It is not local to the blocks it is defined in.

And actually it is a race condition to decide which block will begin executing first.
Assigning a variable is quick, so on most Jenkins runs the two statements:

url = "http://host1/file1"
url = "http://host2/file2"

will be executed very quickly one after another in random order. And only then the downloading will begin.

So, the value "url" could be "http://host1/file1" or "http://host2/file2", chosen randomly in both blocks. On some Jenkins runs, this code will download the contents of "file1" twice and store it as both "file1" and "file2". On other Jenkins runs, it will download "file2" twice.

But actually I saw this job sometimes download the files correctly; on those runs, Jenkins was so loaded that the parallel run was actually executed sequentially. This is why I didn't see the problem immediately.

I seem to recall that Scala 2 only became really fully usable with version 2.10. In Scala 2.10, they added macros and some other essential improvements.

The changelog for Scala 2.10 is impressive indeed:

https://www.scala-lang.org/download/changelog.html

They added futures / promises, string interpolation, added implicit classes (that is, extension methods), and they still needed to fix the pattern matching!

It's fair to say that Scala 2 took a while to get in shape. For example, try/catch/finally was only available in Scala 2.8.

It seems that we are getting a similar deal with Scala 3. New syntax and new language features in each minor release, bugs that prevent your code from working, and a general sense of instability.

I tried to cross-compile some fairly straightforward code with Scala 3.3 and 3.4 but the compiler crashed with a weird bytecode error.
Something along the lines of "cannot emit the Array class".
The Array class was used in the compiler itself, my code didn't use that.

I'm all in favor of Scala 3 improvements but right now it's unusable. I'll wait until Scala 3.10 and try again.

Предположимъ, у насъ фирма по разработкѣ квантовыхъ компьютеровъ. Въ просторномъ залѣ сидятъ 100500 слесарей и паяютъ что-то тамъ. Ни одинъ изъ нихъ никогда не изучалъ ни квантовую механику, ни матанализъ, ни даже перемноженiе матрицъ. Это просто такiе знающiе спецiалисты, они всѣ прошли собесѣдованiя на должность "старшiй слесарь" и имѣютъ 10-15 лѣтъ опыта работы. Когда мы сможемъ ожидать, что квантовый компьютеръ заработаетъ?

(Слесари именно паяютъ, это не опечатка. И почти каждый изъ слесарей говоритъ, что научился паять электронику самъ. "Мнѣ купили дѣтскiй паяльникъ, когда я пошелъ въ школу... Я нигдѣ не учился паять спецiально, потомъ постепенно пришло пониманiе, какъ это надо дѣлать..." и т.д.)

Абсурдная картина. Вѣдь нельзя надѣяться изобрѣсти квантовый компьютеръ, не имѣя понятiя о принципахъ его работы. Но именно такъ выглядитъ сегодняшняя индустрiя программированiя. ( Read more... )

https://www.youtube.com/watch?v=SjhIlw3Iffs

I met Ilya briefly while I lived in San Francisco. He is undoubtedly a deep thinker. There is however one blind spot in his worldview. He believes that large language models (LLMs) already know everything there is to know about reality. He knows that LLMs are trained on human-generated data with human-generated advice. So, he accepts that there is nothing more to know about the world other than what people already know. More precisely, there is nothing more to know than what people have already written on the Internet.

This sort of magical thinking is pervasive in modern fantasy novels. Those novels operate in a world where all knowledge has been already obtained centuries ago. Everything there is to know is already codified in some old books. There is no new knowledge - and there cannot be any. Free thinking is impossible and meaningless. If you want to know how to do something, or if you want to know what something means or what properties something has, all you need is to find a book old enough or thick enough and you will get your answer.

Types with universal quantifiers correspond to "generic functions", that is, functions with a type parameter (or with several type parameters). For example (Scala):

def f[A]: (A, Option[A]) => Option[(A, A)] = {
case (x, oy) => oy.map(y => (x, y))
}

In a more mathematical type notation, the function f has type ∀A. A × (1 + A) → 1 + A × A.

The programmer's intuition for generic functions is that these functions work in the same way for all types. Indeed, the code of f does not depend on the type A and works in the same way for all A.

The requirement of "working in the same way for all types" can be formulated more rigorously: the code can only use a small number of constructions, but may have no side effects, no fixed values of fixed types, no run-time type information, and no calls to external libraries.

For code of that kind, the parametricity theorems, the Yoneda lemma, and the Curry-Howard correspondence hold and can be used for reasoning about the universally quantified types. In many cases, a universally quantified type may be simplified into a type that has no quantifiers.

Here are some examples of simplifying types:
( Read more... )

1. "Covariance" and "contravariance" are properties of a type constructor that follow automatically from the definition of the type constructor. A type constructor is covariant if a `map` function exists and satisfies the functor laws, and contravariant if `contramap` exists and satisfies the contrafunctor laws. If neither `map` nor `contramap` function can be found (e.g., because the type signature cannot be implemented or because the laws cannot be satisfied), the type constructor is neither covariant nor contravariant.

Covariance and contravariance are not labels arbitrarily chosen by the programmer. In Scala, one can declare List[A] without covariance but Option[+A] with covariance. But this makes no sense. List[_] is covariant according to its definition because a `map` function exists with correct properties. It is a problem if the compiler does not recognize the covariance of List[_] automatically.

2. "Subtyping" is a relation between types that requires to have an automatic conversion from one type to another. If A is a subtype of B (we write A <: B), the compiler will automatically insert a conversion function from A to B whenever it is necessary.

If a function `f` is defined to have an argument of type `B`, but the programmer writes `f(x)` where `x` has type `A`, then the compiler will automatically insert a conversion function (say, `a2b` of type A => B) and rewrite `f(x)` into `f(a2b(x))`.

Each compiler defines in its own way what types will be subtypes of others. In Scala, the programmer is able to define an implicit conversion between arbitrary types. So, Scala supports essentially arbitrary subtyping relations. Whether they are useful is up to the programmer.
( Read more... )

I'm trying to find a simple proof of parametricity theorems, without using relations. I hoped that I can use dinatural transformations https://en.wikipedia.org/wiki/Dinatural_transformation directly and prove that any purely functional code of type P[A, A] -> Q[A, A] is a dinatural transformation. However, after starting to write up a proof, I ran into a snag: dinatural transformations do not compose. For example, this paper shows some conditions for them to compose https://drops.dagstuhl.de/opus/volltexte/2018/9700/pdf/LIPIcs-CSL-2018-33.pdf But it seems that I can't restrict programs to those conditions. So I'm stuck.

Выхожу изъ тюрьмы, политикой не занимаюсь... Гляжу - Трампъ подписалъ новый законъ о копирайтѣ. Тутъ одинъ такой въ штатскомъ подходитъ и спрашиваетъ - вы не слышали, а что это за законъ Трампъ подписалъ. Я говорю - кому надо, тому и подписалъ... Выхожу изъ тюрьмы, политикой не занимаюсь...

In a programmer's language, a "category" is "cartesian closed category with a final object".

In Part I I showed that some adjunctions are obtained via the "adjunction completion". However, it remains unclear which functors have non-void completions.

To gather intuition, I limited my consideration to polynomial functors F and their transformations L(F) and R(F), defined by

L(F) a ≡ ∀ i. (a -> F i) -> i

R(F) a ≡ ∃ i. i × (F i -> a)

( Read more... )

After https://git.kernel.org/pub/scm/linux/kernel/git/torvalds/linux.git/commit/?id=8a104f8b5867c682d994ffa7a74093c54469c11f

Our Pledge

In the interest of fostering an environment that is open and welcoming to productive contributors, we pledge to making participation in our project and our community a productive coding and learning experience for everyone, regardless of political views, country of origin, skin color, personal psychological problems and emotional needs, and skills in verbal expression in English or other natural language.

Our Standards

Examples of behavior that contributes to creating a productive environment include:

• Using language focused on the problem at hand, e.g. "in line 123 you used an incorrect function"
  
• Recognizing that a given viewpoint may be valid or invalid, and arguing on the merits, regardless of the perceived popularity or authority
  
• Voicing to-the-point criticism, even though it may offend some people
  
• Focusing on developing code and fixing bugs, not on feeling good about ourselves
  
• Showing a willingness to learn more technical matters as necessary
  

Examples of unacceptable behavior include:

• Accusing others of being "insensitive" or "harassing", instead of responding constructively to technical criticism (such as "you wrote incorrect code in line 123") or to other criticism (such as "you have bad English grammar in the comment in line 120 - you should write more clearly")
  
• Personal or political attacks on people (e.g. calling someone a "white supremacist" or "racist")
  
• Public or private harassment, accompanying demands to conform to a chosen political ideology (e.g. harassing someone who refuses to praise or to condemn persons with a given political opinion)
  
• Demanding that software developers should behave as political activists or as a "thought police" (e.g. pretending that someone's joke was a serious statement and castigating that person for wrong-thinking)
  
• Imposing a discussion of political topics in developer's mailing list or chat channel, and generally steering the discussion away from productive technical subject matter into a politically charged domain
  
• Publishing others’ private information, such as a physical or electronic address, without explicit permission
  

Our Responsibilities

Maintainers are responsible for clarifying the standards of acceptable behavior and are expected to take corrective action in response to consistent unacceptable behavior.

Maintainers have the responsibility to reject comments, commits, code, wiki edits, issues, and other contributions that are not aligned to this Real Code of Conduct, or to ban temporarily or permanently any contributor for behaviors that contradict the Real Code of Conduct.

Scope

This Code of Conduct applies both within project spaces and in public spaces when an individual is representing the project or its community. Examples of representing a project or community include using an official project e-mail address, posting via an official social media account, or acting as an appointed representative at an online or offline event. Representation of a project may be further defined and clarified by project maintainers.

Enforcement

Instances of unacceptable behavior may be reported by contacting the Moderator's Board <xyz@xyz.org>. All complaints will be reviewed and investigated and will result in a response as appropriate to the circumstances, in the opinion of one or more main moderators. The Board is NOT obligated to maintain confidentiality with regard to the reporter of an incident. All details of any action by the Board must be posted immediately.

Maintainers who consistently do not follow or do not enforce the Real Code of Conduct will be dismissed from the Moderator's Board and may be further sanctioned from the project, as any other developers.

"Applied functional type theory" is a tentative name for the theory underlying modern functional programming.

All my technical posts on this topic so far:

2011-01-10 My monad tutorial https://chaource.dreamwidth.org/61718.html

2013-05-24 Lambda-calculus without recursion https://chaource.dreamwidth.org/93438.html

2015-04-09 Exercises in Curry-Howard correspondence https://chaource.dreamwidth.org/125399.html

2016-06-28 Functional programming is physics https://chaource.dreamwidth.org/143497.html

2017-03-26 Functional programming and the real world https://chaource.dreamwidth.org/161590.html

2016-08-30 Example of the use of category theory in functional programming https://chaource.dreamwidth.org/148979.html

2016-05-29 Polynomial functors I. Basic motivations. All polynomial type constructors are functors https://chaource.dreamwidth.org/140652.html

2016-06-01 Polynomial functors II. Basic definitions: (co)pointed, (co)distributive, (co)monadic. Monadic functors are distributive https://chaource.dreamwidth.org/140862.html

2016-06-02 Co-pointed functors are co-distributive https://chaource.dreamwidth.org/141143.html

2016-06-03 Polynomial functors III: all polynomial functors are (co)distributive https://chaource.dreamwidth.org/141503.html

2016-06-05 Polynomial functors IV: all polynomial functors are pre-(co)-monadic https://chaource.dreamwidth.org/141702.html

2016-06-10 Polynomial functors V: recursive functors are (co)distributive https://chaource.dreamwidth.org/141968.html

2016-06-16 Polynomial functors VI: An elementary question about polynomials, or How to characterize pairs of functors with natural transformations between them https://chaource.dreamwidth.org/142433.html

2016-06-22 Polynomial functors VII. Pointed and co-pointed recursive polynomial functors https://chaource.dreamwidth.org/143092.html

2016-06-30 Exponential-polynomial functors, contrafunctors, and profunctors https://chaource.dreamwidth.org/143705.html

2016-07-02 Exponential-polynomial profunctors II. Modularity with respect to a monoid https://chaource.dreamwidth.org/144118.html

2016-07-17 Tutorial on the free monad https://chaource.dreamwidth.org/144787.html

2016-07-19 Functors of functors. Deriving the "free monad". All recursive polynomial functors are pre-monadic https://chaource.dreamwidth.org/145119.html

2016-07-21 Polynomial functors VIII. Some recursive polynomial functors are pre-comonadic https://chaource.dreamwidth.org/145578.html

2016-07-22 Polynomial functors IX. Pre-monadic and pre-comonadic recursive functors https://chaource.dreamwidth.org/145721.html

2016-07-31 Representable functors and GADTs https://chaource.dreamwidth.org/146894.html

2016-08-04 Free functors, free applicatives, free monads I https://chaource.dreamwidth.org/147004.html

2016-08-07 Free functors, free applicatives, free monads II https://chaource.dreamwidth.org/147235.html

2016-08-09 Free functors, free applicatives, free monads III https://chaource.dreamwidth.org/147892.html

2016-08-11 Free functors, free applicatives, free monads IV https://chaource.dreamwidth.org/148057.html

2016-08-31 Initial F-algebras and free F-algebras over a type https://chaource.dreamwidth.org/149039.html

2016-10-04 The center-of-mass monad (also called the search monad) https://chaource.dreamwidth.org/150558.html

2017-03-05 All (recursive) polynomial functors are traversable https://chaource.dreamwidth.org/160254.html

2017-03-06 Monad transformers for exp-polynomial monads I https://chaource.dreamwidth.org/160492.html

2017-03-08 Monad transformers for exp-polynomial monads II https://chaource.dreamwidth.org/160598.html

2017-03-10 Exponential-polynomial applicative functors https://chaource.dreamwidth.org/160849.html

2017-03-13 Exponential-polynomial monads https://chaource.dreamwidth.org/161043.html

2017-03-19 Contrafunctors cannot be distributive or traversable https://chaource.dreamwidth.org/161356.html

2017-04-03 Monad transformers and free monads https://chaource.dreamwidth.org/161968.html

2017-04-15 Monads and monad transformers: The errors of my ways https://chaource.dreamwidth.org/162150.html

2018-03-03 The ubiquitous premonads: The simplest way to formulate monad laws https://chaource.dreamwidth.org/170783.html

2018-03-04 Monoids and co-monoids https://chaource.dreamwidth.org/171355.html

2018-04-03 Some polynomial functors are not monadic? https://chaource.dreamwidth.org/172218.html

2018-04-07 Some polynomial functors are not monads https://chaource.dreamwidth.org/173033.html

2018-05-28 Applicative profunctors https://chaource.dreamwidth.org/174611.html

2018-10-09 Adjoint functors in functional programming https://chaource.dreamwidth.org/182694.html

2018-10-11 Adjoint functors in functional programming II https://chaource.dreamwidth.org/183087.html

2018-11-27 The upside-down polynomial transformation https://chaource.dreamwidth.org/184360.html

2019-01-16 Quantified types are undecidably powerful https://chaource.dreamwidth.org/186193.html

2019-02-14 Some monads do not have a corresponding monad transformer? https://chaource.dreamwidth.org/186744.html