Crash Course on Notation in Programming Language Theory

This blog post is meant to help my friends get started in reading my other blog posts, that is, this post is a crash course on the notation ...

Crash Course on Notation in Programming Language Theory

This blog post is meant to help my friends get started in reading my other blog posts, that is, this post is a crash course on the notation ...

Don’t Implement Unification by Recursion

Unification is formal methods speak for solving equations.

How to Teach Writing Research Papers

Parenthetically Speaking: Articles by Shriram Krishnamurthi

Nikita Karetnikov

Gentle intro to type-level recursion in Rust: from zero to HList sculpting.

Implementing plucking from and shaping of HLists in Frunk: getting the type signature right was 99% of the work. Here's what I've learnt along the way.

The algebra (and calculus!) of algebraic data types

The Flix Programming Language

Pattern Types ⊆ Refinement Types - HackMD

I spends the last 8

The borrow checker within · baby steps

graydon2 | Some notes on Rust, mutable aliasing and formal verification

Hello, you've been (semi-randomly) selected to take a CAPTCHA to validate
your requests. Please complete it below and hit the button!

Polarized Subtyping: Code/Artifact

Artifact accompanying the paper Polarized Subtyping, published in the proceedings of ESOP 2022. We've included an extended version of the paper with this submission (2201.10998.pdf), which is also available directly on arXiv. Docker Image: The artifact is packaged as a docker container. The docker image is available on Github Packages, under the esop22 tag. We've also included the docker image as a .tar file (polite-esop:esop22.docker.tar), which can be loaded directly via: % docker load polite-esop:esop22.docker.tar Source Code: All of the software, source code (the Polite programming language), and related files are packaged within the docker container (available on Github Packages and in this submission). Follow the steps below (or in README.txt), to pull the docker image, run it, and run the paper-related examples, i.e. the `.polsub` files. We've also included these files as part of this submission for posterity: bin.polsub emptyfull.polsub examples.polsub omega.polsub stream.polsub Getting Started Guide 1. Pull down the public docker image: % docker pull ghcr.io/zeeshanlakhani/polite-esop:esop22 2. Run the docker container interactively: % docker run --rm -it --name polite-esop ghcr.io/zeeshanlakhani/polite-esop:esop22 Of note, this is a x86-64/amd64 (Intel) built container. The artifact will not run on arm64 hosts (e.g. an M1 macbook). 3. After running step 2., you'll enter into the designated `/polite/esop22` directory within the container, where there are 5 example `.polsub` files to run, associated with the paper submission. You can use the `polite` executable (already in the PATH) to view the output of each example: % polite bin.polsub % polite emptyfull.polsub % polite examples.polsub % polite omega.polsub % polite stream.polsub 4. To run examples and view purposeful typechecking errors in relation to subtyping, then run any of the examples above with the `-d` debug flag: % polite -d bin.polsub 5. Additionally, you can run the examples interactively in SML/NJ (by first runningÂ `sml`): CM.make "../src/sources.cm"; Top.polite "bin.polsub"; Top.polite "emptyfull.polsub"; Top.polite "examples.polsub"; Top.polite "omega.polsub"; Top.polite "stream.polsub"; Step by Step Instructions Now, we'll walk through each of the `polsub` programs in `/polite/esop22`, which exhibit key examples in and claims made by the paper. Throughout the example programs, `[stream0]` and `(thunk stream0)` are interchangeable, as is `y` and `return y`, where using `thunk` and `return` matches to how we express thunk values and return computations in the paper. As in the paper, our bidirectional typechecking algorithm is polarized. As is evident from the bidirectional rules, A : B, for positive types A and B, will hold exactly when `fun x = x : A - B`. Similarly, for negative types A and B, A : B is true exactly if `fun x = force x : [A] - B`. We use this in some of the examples to verify or refute some subtyping relations. 1. % polite -d examples.polsub This program demonstrates general type examples used throughout the paper, including much of what exists in Appendix A (in the extended version of the paper). Samples include: `nat` and `bool` (positive) variant records types, how `list` or `queue` datatypes would be constructed, identity functions mutually recursive `even` and `odd` datatypes, a simple, incorrect function type computation in `succ'` 2. % polite -d bin.polsub This program demonstrates our first example in Section 2.2, where we expect the subtyping relationships `pos` = `std` = `bin` to hold, as every positive standard number is a standard number, and every standard number is a binary number. The `fail` keyword showcases where subtyping is expected to fail. The precise locations of the errors are propagated when using the `-d` flag, e.g. ./esop22/bin.polsub:31.38-31.44:error:subtyping fails: std not : pos | 'b1 x2 = 'b0 x2 } `eval` evaluates computation expression, e.g. `ten`, `eleven`, etc. The `inc`, `dec0` functions match up with our claims in the paper, where `dec0` should indeed fail. Of note, the `dec` example in the first version of our paper had a typo, which we demonstrate the failure of in `dectypo`. We show the correct version with the computation `dec` and have already made the change in the available submission. 3. % polite stream.polsub This program demonstrates our second example in Section 2.2, where we have an example of a type with mixed polarities: a stream of `std` binary numbers with a finite amount of padding between consecutive numbers. As in the paper, we present padded streams as mutually dependent type definitions, one positive and one negative. `zstream` demonstrates the usefulness of variant records with one alternative `'some`. The expressions `compress` and `omit` are two mutually recursive functions used to generate a stream with zero padding from a stream of arbitrary (but finite) padding. `compress'`, `omit'` and the evaluation of `stream0'` are used here just to establish how the language implementation can interchangeably use `[a]` for `thunk a` and `b` for `return b`, where the latter of each is used in the paper, but is more cumbersome for writing programs. Evaluated expressions `stream0` and `stream1` validate how we can actuallycompress a padded stream into one with zero padding! 4. % polite omega.polsub This program demonstrates our third example in Section 2.2, where we consider the embedding of the untyped lambda calculus in a polarized setting, e.g. (U^- : [U] - U), and highlight the notion of semantic typing and how it ensures behavioral soundness. As in the paper, `omega` and `Omega` are equirecursive type definitions and well-typed even though the evaluation of `Omega` would diverge (i.e. never terminate). The commented-out `eval nontermination` showcases this and, indeed, would never terminate if actually executed. 5. % polite -d emptyfull.polsub Here we demonstrate examples in relation to our presentation of "emptiness" and "fullness" in the paper (Semantic Subtyping, Section 4.1). In this program, we showcase how to check for the emptiness and fullness of types with our implementation. For positive types, we check that a type t is empty by typechecking an identity function from t into an empty type (`ex1`, `ex3`). If typechecking the identity function from a positive type t to an empty type fails, we conclude that the type is not empty (`ex2`, `ex4`). For negative types, we can use our implementation to check when full types are supertypes of other types (`inf_sub_top`, `inf_sub_emp`) and when a type (e.g. `inf`) is not full by checking that the typechecking of an identity function from a full type fails (`top_nsub_inf`, `comp emp_nsub_inf`). The 5 programs above illustrate various examples related to our paper and show that our language implementation, Polite, works faithfully and as expected. Outside of the esop22 directory, (e.g. % cd /polite), we include all of the source code for the implementation, as well as more examples and regression tests, which include our ongoing and future work: adding intersections and unions to polarizing subtyping. The `polite.readme.txt` in the `/polite` directory also shows our language's grammar. Files (in the container) /polite/esop22/ -- ESOP22 paper-related examples and documentation /polite/src/ -- implementation in SML /polite/examples/ -- some example programs, some of which include intersection and union (sub)typing /polite/tests/ -- regression tests /polite/polite.readme.txt -- general documentation for the Polite programming language implementation Description An implementation of the Polite programming language based on call-by-push-value, equirecursive types, subtyping, and intersection and union types. The language version with subtyping but without intersections and unions is described in: Polarized Subtyping Zeeshan Lakhani, Ankush Das, Henry DeYoung, Andreia Mordido, Frank Pfenning European Symposium on Programming (ESOP 2022) Contributors (implementation): Zeeshan Lakhani Frank Pfenning Contributors (theory): Ankush Das Henry DeYoung Andreia Mordido

Aplas11

Kell14in author version

journal.stuffwithstuff.com

[Haskell'23] The Evolution of Effects

The Evolution of Effects (Keynote) (Video, Haskell 2023)
Nicolas Wu
(Imperial College London, UK)
Abstract: Functional programming has been celebrated for its promise of pure functions, delivering referential transparency and elegant reasoning about programs. However, real-world applications are not pure, and necessitate interaction with the outside world, introducing computational effects such as IO, state, and exceptions. The journey to harmonize these seemingly contradictory paradigms has led to a fascinating evolution of effectful programming in Haskell.
The introduction of monads as a practical programming tool was a pivotal discovery, enabling controlled sequencing of effectful computations and addressing the challenge of handling side effects in a pure language. However, it soon became evident that the lack of modularity in composing effects using monads posed a limitation to effectful programming. To overcome this obstacle, monad transformers emerged as a solution, providing a composable manner of building effects on top of one another.
More recent advancements have led to algebraic effects as an alternative framework that is easy to extend, particularly as domain-specific languages crafted to work in specific contexts. Nevertheless, these effects are not without quirks and limitations, leading to the development of higher-order effects. These higher-order effects extend the capabilities of algebraic effects, providing greater flexibility for expressing effectful computations, while also shedding light on the connection between the monad approach and the algebraic approach to effects.
This talk will survey the historical milestones that have shaped the landscape of effectful programming in Haskell, exploring the transition from monads to monad transformers and the emergence of algebraic and higher-order effects.
Article: https://doi.org/10.1145/3609026.3615581
ORCID: https://orcid.org/0000-0002-4161-985X
Video Tags: icfpws23haskellmain-key2-p, doi:10.1145/3609026.3615581, orcid:0000-0002-4161-985X
Presentation at the Haskell 2023 conference, September 8–9, 2023, https://icfp23.sigplan.org/home/haskellsymp-2023
Sponsored by ACM SIGPLAN, https://www.sigplan.org/

Introduction - Counterexamples in Type Systems

Context Sensitive Subtyping

Programming with Refinement Types

A refinement type by any other name | weaselhat

Semantic Subtyping in Luau

Luau is the first programming language to put the power of semantic subtyping in the hands of millions of creators.

Off-the-shelf semantic subtyping is slightly different from what is implemented in Luau, because it requires models to be set-theoretic, which requires that inhabitants of function types “act like functions.” There are two reasons why we drop this requirement.

Set-theoretic semantic subtyping does not support this normalization, and instead normalizes functions to disjunctive normal form (unions of intersections of functions). We do not do this for ergonomic reasons: overloaded functions are idiomatic in Luau, but DNF is not, and we do not want to present users with such non-idiomatic types.

For these two reasons (which are largely about ergonomics rather than anything technical) we drop the set-theoretic requirement, and use pragmatic semantic subtyping.

Unexpectedly, this is not always true in set-theoretic models, due to uninhabited types. In set-theoretic models, if x has type never then f(x) has type never. We do not want to burden users with the idea that function application has a special corner case, especially since that corner case can only arise in dead code.

The other difference between Luau’s type system and off-the-shelf semantic subtyping is that Luau does not support all negated types.

The Better Parts. Douglas Crockford. JS Fest 2018

"the bugs that keep you up at night, the type system does not help with those".. and "actually helps to cause those" "you have to circumvent the type system" "you tend to give the type system the value of all of the bugs that it found, but we don't subtract the value of the bugs that it missed" "and we don't consider the value of bugs that it caused" "full accounting of types, they're just not work it"

Two little interpreters

Universal domain types

A guide to domain-specific types that make sense.

I'm betting on Call-by-Push-Value

- bring up for research

Template for CMU SCS PhD thesis (2006)

21 ordered

Ordered logic , cut reduction

Down and Dirty with Semantic Set-theoretic Types (a tutorial) v0.4

Semantic Subtyping in Luau - Roblox Blog

Luau is the first programming language to put the power of semantic subtyping in the hands of millions of creators. Minimizing false positives One of the issues with type error reporting in tools like the Script Analysis widget in Roblox Studio is false positives. These are warnings that are artifacts of the analysis, and don’t correspond […]

Linear Types One-Pager

Oxidizing OCaml: Locality

Coming from OCaml, the Rust programming language has many appealingfeatures. Rust’s system for tracking lifetime and ownership allowsusers to safely express...