Jan Liam Verter lambduli

Approachable PL Papers for Undergrads

On September 28, 2021, I asked on Twitter:

PL Twitter:

you get to recommend one published PL paper for an undergrad to read with oversight by someone experienced. the paper should be interesting, approachable, and (mostly) self-contained.

what paper do you recommend?

What I Didn't Know about Functional Programming until 2020

Programming using a series of transformations and aggregations, something I've been doing for years, is known as programming in the map/reduce style.
The more abstract the type is, the greater its cardinality, and the smaller the set of operations it supports. So make use of universal quantifiers, particularly by implementing fully parametric functions. They guide you on how to implement their term-level definitions by narrowing down the number of possible implementations. In other words, the type system of Scala (or Haskell, for that matter) is not only great for capturing compile-time errors, but is also capable of leading you to the correct solution.
You can encode union types by combining different Scala features such as type constructors, subtyping and implicits, and by taking advantage of the Curry-Howard Isomorphism and De Morgan's Laws for neg

Statically checked overloaded strings

This gist demonstrates a trick I came up with which is defining IsString for Q (TExp a), where a is lift-able. This allows you to write $$("...") and have the string parsed at compile-time.

On GHC 9, you are able to write $$"..." instead.

This offers a light-weight way to enforce compile-time constraints. It's basically OverloadedStrings with static checks. The inferred return type

Conferences

Hydraconf

Summer School

Summer school on practice and theory of Distributed Computing

Books

The Cabal/Stack Disambiguation Guide

One of the most frequently asked Haskell beginner questions in recent years is:

"Stack or cabal?"

I will helpfully not answer this question. Instead I will hope to eliminate the confusion that many of the askers seem to have about the various different

Note:

When this guide is more complete, the plan is to move it into Prepack documentation.
For now I put it out as a gist to gather initial feedback.

A Gentle Introduction to Prepack (Part 1)

If you're building JavaScript apps, you might already be familiar with some tools that compile JavaScript code to equivalent JavaScript code:

Babel lets you use newer JavaScript language features, and outputs equivalent code that targets older JavaScript engines.

I think I’ve figured out most parts of the cubical type theory papers; I’m going to take a shot to explain it informally in the format of Q&As. I prefer using syntax or terminologies that fit better rather than the more standard ones.

Q: What is cubical type theory?

A: It’s a type theory giving homotopy type theory its computational meaning.

Q: What is homotopy type theory then?

A: It’s traditional type theory (which refers to Martin-Löf type theory in this Q&A) augmented with higher inductive types and the univalence axiom.

Reading

Title	Author(s)	Year
Intuitionistic Type Theory	Per Martin-Löf	1984
On the Meanings of the Logical Constants and the Justification of the Logical Laws	Per Martin-Löf	1996
[[http://mat.uab.cat/~kock/crm/h

	module Euclid

	import Syntax.PreorderReasoning

	%default total

	Divides : (divisor, dividend : Nat) -> Type
	Divides d n = (q : Nat ** (n = q * d))

	data Direction = LTR \| RTL

	# NOTE:
	# For details on warnings: https://downloads.haskell.org/~ghc/master/users-guide/using-warnings.html
	#
	# This list taken from https://medium.com/mercury-bank/enable-all-the-warnings-a0517bc081c3
	ghc-options:
	- -fwarn-tabs # Warn on tabs (spaces are better)

	- -Weverything # Enable all warnings with -Weverything, then
	# disable the ones we don’t care about