Recently I looked again at PHOAS, and once again I concluded it's nice for library APIs, but so painful to do anything with inside those libraries. So let convert to something else, like de Bruijn.

There are standalone source files if you just want to see the code:

• Agda: https://github.com/phadej/nbexp/blob/master/src/NbEXP/SelfContained/Conv.agda
• Haskell: https://github.com/phadej/nbexp/blob/master/src-hs/Conv.hs

How to convert PHOAS terms to de Bruijn terms?

The solution is hard to find.

You can cheat, [as mentioned by Roman on Agda mailing list https://lists.chalmers.se/pipermail/agda/2018/010033.html]:

There is always a way to cheat, though. You can turn the PHOAS -> untyped de Bruijn machinery into the PHOAS -> typed de Bruijn machinery by checking that future contexts indeed extend past contexts and throwing an error otherwise (which can't happed, because future contexts always extend past contexts, but it's a metatheorem).

In "Generic Conversions of Abstract Syntax Representation" by Steven Keuchel and Johan Jeuring, authors also "cheat" a bit. The "Parametrhic higher-order abstract syntax" section ends with a somewhat disappointing

  where postulate whatever : _

Keuchel and Jeuring also mention "Unembedding Domain-Specific Languages" by Robert Atkey, Sam Lindley and Jeremy Yallop; where there is one unsatisfactory ⊥ (undefined in Haskell) hiding.

I think that for practical developments (say a library in Haskell), it is ok to make a small short cut; but I kept wondering isn't there is a way to make a conversion without cheating.

Well... it turns out that we cannot "cheat". Well-formedness of PHOAS representation depends on parametricity, and the conversion challenge seems to requires a theorem which there are no proof in Agda.

In unpublished (?) work Adam Chlipala shows a way to do the conversion without relying on postulates http://adam.chlipala.net/cpdt/html/Intensional.html; but that procedure requires an extra well formedness proof of given PHOAS term.

This Agda development is a translation of that developement.

Common setup

Our syntax representations will be well-typed, so we need types:

-- Types
data Ty : Set where
  emp : Ty
  fun : Ty → Ty → Ty

Ctx : Set
Ctx = List Ty

variable
  A B C : Ty
  Γ Δ Ω : Ctx
  v : Ty → Set

de Bruijn syntax

Var : Ctx → Ty → Set
Var Γ A = Idx A Γ -- from agda-np, essentially membership relation.

data DB (Γ : Ctx) : Ty → Set where
  var : Var Γ A → DB Γ A
  app : DB Γ (fun A B) → DB Γ A → DB Γ B
  lam : DB (A ∷ Γ) B → DB Γ (fun A B)
  abs : DB Γ emp → DB Γ A

Parametric Higher-order abstract syntax

data PHOAS (v : Ty → Set) : Ty → Set where
  var : v A → PHOAS v A
  app : PHOAS v (fun A B) → PHOAS v A → PHOAS v B
  lam : (v A → PHOAS v B) → PHOAS v (fun A B)
  abs : PHOAS v emp → PHOAS v A

-- closed "true" PHOAS terms.
PHOAS° : Ty → Set₁
PHOAS° A = ∀ {v} → PHOAS v A

de Bruijn to PHOAS

This direction is trivial. An anecdotal evidence that de Bruijn representation is easier to transformation on.

phoasify : NP v Γ → DB Γ A → PHOAS v A
phoasify γ (var x)   = var (lookup γ x)
phoasify γ (app f t) = app (phoasify γ f) (phoasify γ t)
phoasify γ (lam t)   = lam λ x → phoasify (x ∷ γ) t
phoasify γ (abs t)   = abs (phoasify γ t)

Interlude: Well-formedness of PHOAS terms

dam Chlipala defines an equivalence relation between two PHOAS terms, exp_equiv in Intensional, wf in CPDT book). e only need a single term well-formedness so can do a little less

The goal is to rule out standalone terms like

module Invalid where
  open import Data.Unit using (⊤; tt)

  invalid : PHOAS (λ _ → ⊤) emp
  invalid = var tt

Terms like invalid cannot be values of PHOAS°, as all values of "v" inside PHOAS° have to originated from lam-constructor abstractions. We really should keep v parameter free, i.e. parametric, when constructing PHOAS terms.

The idea is then to simply to track which variables (values of v) are intoduced by lambda abstraction.

data phoasWf {v : Ty → Set} (G : List (Σ Ty v)) : {A : Ty} → PHOAS v A → Set
 where
  varWf : ∀ {A} {x : v A}
    → Idx (A , x) G
    → phoasWf G (var x)
  appWf : ∀ {A B} {f : PHOAS v (fun A B)} {t : PHOAS v A}
    → phoasWf G f
    → phoasWf G t
    → phoasWf G (app f t)
  lamWf : ∀ {A B} {f : v A → PHOAS v B}
    → (∀ (x : v A) → phoasWf ((A , x) ∷ G) (f x))
    → phoasWf G (lam f)
  absWf : ∀ {A} {t : PHOAS v emp}
    → phoasWf G t
    → phoasWf G (abs {A = A} t)

-- closed terms start with an empty G
phoasWf° : PHOAS° A → Set₁
phoasWf° tm = ∀ {v} → phoasWf {v = v} [] tm

A meta theorem is then that all PHOASᵒ terms are well-formed, i.e.

meta-theorem-proposition : Set₁
meta-theorem-proposition = ∀ {A} (t : PHOAS° A) → phoasWf° t

As far as I'm aware this proposition cannot be proved nor refuted in Agda.

de Bruijn to PHOAS translation creates well-formed PHOAS terms.

As a small exercise we can show that phoasify of closed de Bruijn terms creates well-formed PHOAS terms.

toList : NP v Γ → List (Σ Ty v)
toList []       = []
toList (x ∷ xs) = (_ , x) ∷ toList xs

phoasifyWfVar : (γ : NP v Γ) (x : Var Γ A) → Idx (A , lookup γ x) (toList γ)
phoasifyWfVar (x ∷ γ) zero    = zero
phoasifyWfVar (x ∷ γ) (suc i) = suc (phoasifyWfVar γ i)

phoasifyWf : (γ : NP v Γ) (t : DB Γ A) → phoasWf (toList γ) (phoasify γ t)
phoasifyWf γ (var x)   = varWf (phoasifyWfVar γ x)
phoasifyWf γ (app f t) = appWf (phoasifyWf γ f) (phoasifyWf γ t)
phoasifyWf γ (lam t)   = lamWf λ x → phoasifyWf (x ∷ γ) t
phoasifyWf γ (abs t)   = absWf (phoasifyWf γ t)

phoasifyWf° : (t : DB [] A) → phoasWf° (phoasify [] t)
phoasifyWf° t = phoasifyWf [] t

PHOAS to de Bruijn

The rest deals with the opposite direction.

In Intensional Adam Chlipala uses v = λ _ → ℕ instatiation to make the translation.

I think that in the typed setting using v = λ _ → Ctx turns out nicer.

The idea in both is that we instantiate PHOAS variables to be de Bruijn levels.

data IsSuffixOf {ℓ} {a : Set ℓ} : List a → List a → Set ℓ where
  refl : ∀ {xs} → IsSuffixOf xs xs
  cons : ∀ {xs ys} → IsSuffixOf xs ys → ∀ {y} → IsSuffixOf xs (y ∷ ys)

We need to establish well-formedness of PHOAS expression in relation to some context Γ

Note that variables encode de Bruijn levels, thus the contexts we "remember" in variables should be the suffix of that outside context.

wf : (Γ : Ctx) → PHOAS (λ _ → Ctx) A → Set
wf {A = A} Γ (var Δ)         = IsSuffixOf (A ∷ Δ) Γ
wf         Γ (app f t)       = wf Γ f × wf Γ t
wf         Γ (lam {A = A} t) = wf (A ∷ Γ) (t Γ)
wf         Γ (abs t)         = wf Γ t

And if (A ∷ Δ) is suffix of context Γ, we can convert the evidence to the de Bruijn index (i.e. variable):

makeVar : IsSuffixOf (A ∷ Δ) Γ → Var Γ A
makeVar refl     = zero
makeVar (cons s) = suc (makeVar s)

Given the term is well-formed in relation to context Γ we can convert it to de Bruijn representation.

dbify : (t : PHOAS (λ _ → Ctx) A) → wf Γ t → DB Γ A
dbify         (var x)   wf        = var (makeVar wf)
dbify         (app f t) (fʷ , tʷ) = app (dbify f fʷ) (dbify t tʷ)
dbify {Γ = Γ} (lam t)   wf        = lam (dbify (t Γ) wf)
dbify         (abs t)   wf        = abs (dbify t wf)

What is left is to show that we can construct wf for all phoasWf-well-formed terms.

Adam Chlipala defines a helper function:

makeG′ : Ctx → List (Σ Ty (λ _ → Ctx))
makeG′ [] = []
makeG′ (A ∷ Γ) = (A , Γ) ∷ makeG′ Γ

However for somewhat technical reasons, we rather define

expand : (Γ : Ctx) → NP (λ _ → Ctx) Γ
expand []      = []
expand (_ ∷ Γ) = Γ ∷ expand Γ

and use expand with previously defined toList to define our version of makeG:

makeG : Ctx → List (Σ Ty (λ _ → Ctx))
makeG Γ = toList (expand Γ)

makeG and makeG′ are the same:

toList∘expand≡makeG : ∀ Γ → makeG Γ ≡ makeG′ Γ
toList∘expand≡makeG []      = refl
toList∘expand≡makeG (A ∷ Γ) = cong ((A , Γ) ∷_) (toList∘expand≡makeG Γ)

Then we can construct wf for all phoasWf:

wfWfVar : Idx (A , Δ) (makeG Γ) → IsSuffixOf (A ∷ Δ) Γ
wfWfVar {Γ = B ∷ Γ} zero    = refl
wfWfVar {Γ = B ∷ Γ} (suc i) = cons (wfWfVar i)

wfWf : (t : PHOAS (λ _ → Ctx) A) → phoasWf (makeG Γ) t → wf Γ t
wfWf         (var x)   (varWf xʷ)    = wfWfVar xʷ
wfWf         (app f t) (appWf fʷ tʷ) = wfWf f fʷ , wfWf t tʷ
wfWf {Γ = Γ} (lam f)   (lamWf fʷ)    = wfWf (f Γ) (fʷ Γ)
wfWf         (abs t)   (absWf tʷ)    = wfWf t tʷ

And finally we define dbifyᵒ for all well-formed PHOASᵒ terms.

dbify° : (t : PHOAS° A) → phoasWf° t → DB [] A
dbify° t w = dbify t (wfWf t w)

Bonus section

We can show that converting closed de Bruijn term to PHOAS and back is an identity function:

bonus-var : (x : Var Γ A) → x ≡ makeVar (wfWfVar (phoasifyWfVar (expand Γ) x))
bonus-var {Γ = A ∷ Γ} zero    = refl
bonus-var {Γ = A ∷ Γ} (suc i) = cong suc (bonus-var i)

bonus : (t : DB Γ A)
      → t ≡ dbify (phoasify (expand Γ) t)
              (wfWf (phoasify (expand Γ) t) (phoasifyWf _ t))
bonus (var x)   = cong var (bonus-var x)
bonus (app f t) = cong₂ app (bonus f) (bonus t)
bonus (lam t)   = cong lam (bonus t)
bonus (abs t)   = cong abs (bonus t)

bonus° : ∀ (t : DB [] A) → t ≡ dbify° (phoasify [] t) (phoasifyWf° t)
bonus° t = bonus t

Normalization by evaluation using parametric higher order syntax. In Agda.

I couldn't find a self-contained example of PHOAS NbE, so here it is. I hope someone might find it useful.

module NbEXP.PHOAS where

data Ty : Set where
  emp : Ty
  fun : Ty → Ty → Ty

data Tm (v : Ty → Set) : Ty → Set where
  var : ∀ {a} → v a → Tm v a
  app : ∀ {a b} → Tm v (fun a b) → Tm v a → Tm v b
  lam : ∀ {a b} → (v a → Tm v b) → Tm v (fun a b)

data Nf (v : Ty → Set) : Ty → Set
data Ne (v : Ty → Set) : Ty → Set

data Ne v where
  nvar : ∀ {a} → v a → Ne v a
  napp : ∀ {a b} → Ne v (fun a b) → Nf v a → Ne v b

data Nf v where
  neut : Ne v emp → Nf v emp
  nlam : ∀ {a b} → (v a → Nf v b) → Nf v (fun a b)

Sem : (Ty → Set) → Ty → Set
Sem v emp       = Ne v emp
Sem v (fun a b) = Sem v a → Sem v b

lower : ∀ {v : Ty → Set} (a : Ty) → Sem v a → Nf v a
raise : ∀ {v : Ty → Set} (a : Ty) → Ne v a → Sem v a

lower emp       s = neut s
lower (fun a b) s = nlam λ x → lower b (s (raise a (nvar x)))

raise emp       n   = n
raise (fun a b) n x = raise b (napp n (lower a x ))

eval : {v : Ty → Set} {a : Ty} → Tm (Sem v) a → Sem v a
eval (var x)   = x
eval (app f t) = eval f (eval t)
eval (lam t) x = eval (t x)

nf : {a : Ty} → {v : Ty → Set} → Tm (Sem v) a → Nf v a
nf {a} t = lower a (eval t)

nf_parametric : {a : Ty} → ({v : Ty → Set} → Tm v a) -> ({v : Ty → Set} → Nf v a)
nf_parametric t = nf t

In hashable-1.4.5.0 I made it use a XXH3 algorithm for hashing byte arrays. The version 1.4.5.0 and 1.4.6.0 backlashed, as I enabled -march=native by default, and that causes distribution issues. Version 1.4.7.0 doesn't enable -march=native by default.

This by default leaves some performance on the table, e.g. a quick benchmark comparison on my machine (model name: AMD Ryzen Threadripper 2950X 16-Core Processor) gives

Benchmark              without   with            
hash/Text/strict/11    1.481e-8  1.289e-8 -12.95%
hash/Text/strict/128   0.319e-7  0.263e-7 -17.73%
hash/Text/strict/2^20  2.220e-4  1.252e-4 -43.61%
hash/Text/strict/40    1.934e-8  1.714e-8 -11.37%
hash/Text/strict/5     1.194e-8  0.995e-8 -16.64%
hash/Text/strict/512   0.778e-7  0.649e-7 -16.62%
hash/Text/strict/8     1.215e-8  0.983e-8 -19.09%
Geometric mean         0.810e-7  0.644e-7 -20.47%

i.e. the new default is 15% slower for small inputs (which is probably the use case for hashable), and it gets worse for larger ones.

https://hackage.haskell.org/package/xxhash-ffi-0.3/xxhash-ffi.cabal doesn't give any control to the user, specifically; there's also a bit of non-determinism because the pkg-config flag is automatic - you may not notice which version you use, having libxxhash-dev installed is rare, but it may happen. (So if you have package xxhash-ffi cc-options: -march=native, it might be not used, if you forget to force off the pkg-config flag).

architecture selection and chip optimizations

Which made me wonder, how much this kind of very low-level performance optimisation we leave on the table when we only care about running binaries locally (e.g. tests; but also benchmarks).

For example, popCount is relatively common, https://hackage-search.serokell.io/?q=popCount says 1948 matches across 196 packages; and includes things like vector-algorithms which one would hope to be fast. countLeadingZeros is also common with 541 matches across 114 packages (and 532 matches across 82 package for countTrailingZeros including unordered-containers).

To get the popcnt operation you need to enable msse4.2, to get lzcnt instead of bsr you need to enable -mbmi2. popCount fallback is a loop, it's slow (I was thinking about that when I wrote splitmix in 2017; however there popCount is not used in hot path; except if you split a lot... like you do when using QuickCheck's Gen... hopefully doesn't matter... does it?). This StackOverflow answer says that there is no fallback from lzcnt to bsr, but maybe it's LZCNT == (31 - BSR) as accepted answer says. I'm not an expert in x86 ISA; nor I want to be writing Haskell; I hope there was some good reason to introduce LZCNT, and it's worth using when it exists.

I don't think many people add

package *
  ghc-options: -msse4.2 -mavx -mbmi -mbmi2

to their cabal.project.local files. Does it matter? I hope that shouldn't make anything worse (except the portability).

There are few small issues with code generation like https://gitlab.haskell.org/ghc/ghc/-/issues/25019 or https://gitlab.haskell.org/ghc/ghc/-/issues/24989, I'm sure these will be fixed soon.

However, I'm not so optimistic about bigger issues like adding arch=native and also -mtune=...; as far as I understand, architecture flags tell compiler that it can or cannot use some instructions, where mtune is an optimization flag. Even if some instruction is supported by a chip, it doesn't mean it's fast (but maybe it's more relevant for SIMD stuff). That's knowledge I hope compiler to know better than me.

Or even bigger ones to decide whether -march=native -mtune=native should be default. Arguably, e.g. GCC and Clang produce very portable binaries by default, but at least they have convenient enough ways to tune binaries for local execution too.

text

This low-level instruction business is surprisingly common. E.g. text uses simdutf except your text probably doesn't because GHC ships text without simdutf (as currently around GHC-9.10.1 time). The text doesn't suffer from -march=native issue like hashable, at least partially because of the above. I'm not sure how the things work there, it looks like simdutf compiles code for various processors:

#define SIMDUTF_TARGET_HASWELL SIMDUTF_TARGET_REGION("avx2,bmi,pclmul,lzcnt")
#define SIMDUTF_TARGET_WESTMERE SIMDUTF_TARGET_REGION("sse4.2,pclmul")

and then uses dynamic dispatch. Or maybe the sse4.2 is just so common nowadays, that the few rare people who compile text themselves don't run into portability issues. (GHC only enables sse2 for Haskell code

text also has some non-simdutf code too as e.g. the issue about avx512 detection highlights; and that uses dynamic dispatch as far as I can tell. (What's the cost of dynamic dispatch? I doubt it's free, and when the operations are small it might show, does it?)

Given all that, I think that it won't hurt if one could compile text so there aren't runtime ISA-detection (so things can be tuned for your chip), even if the default were to do a runtime dispatch. (e.g. if we had that, there would be an immediate workaround for above avx512 detection issue: explicitly turn it off). And again, it would be nice if GHC and cabal-install had convenient ways to enable for-local-execution optimisations (and for bundled libraries like text it's almost impossible nowadays, due no good way to force their re-installation, Cabal#8702 is a related issue).

containers

containers also use popCount, countLeadingZeros; but I bet that it's always used with the portable configuration in practice, as it's bundled with GHC, similarly as text library is. (The IntSet / IntMap implementation uses bit level operations, it might benefit from using better instructions when available).

Conclusion

It feels that the end of compilation pipeline - the assembly generation - isn't getting as much attention as it could¹. Sure, these improvements would only decrease run times constant factors only. On the other hand, if we could get 2-3% improvements in hot loops without source code changes, why not get these?

I'm biased, (not only) as maintainer of hashable I would like to see CLMUL instruction, and AESENC would be nice to play with. But if I the 99.9% used default would rely on their software fallbacks rather than fast silicon implementation, I bet there won't be anything interesting to discover.

And it would be nice to have CPP macros to reflect whether GHC will generate POPCNT, LZCNT, CLMUL, AESENC instruction or their fallbacks. E.g. in hashable it's worth using AESENC for mixing if it's a silicon one, otherwise it's probably better to stick to a different but simpler fallback. (Maybe we already has these: GHC#7554 suggests so, maybe it's only a documentation issue GHC#25021).

cabal-fields is partly motivated by the Migrate from the .cabal format to a widely supported format issue. Whether it's a solution or not, it's up to you to decide.

Envelope grammar vs. specific format grammar

It is important to separate the envelope format (whether it's JSON, YAML, TOML, or cabal-like) from the actual file format (package.json, stack.yaml, Cargo.toml, or pkg.cabal for various package description formats).

An envelope format provides the common syntax. Often it has special support for enumerations i.e. lists. cabal-like format doesn't. All fields are just opaque text. Depending on how you look at it, that's the good or bad thing.

Surely, specifying build dependencies like:

dependencies:
  - base >= 4.13 && < 5
  - bytestring

makes the list structure clear for consumers. However, e.g. hpack doesn't use list syntax uniformly: ghc-options, which is a list-typed field, is still an opaque text field in hpack package description.

And individual package dependencies are also just opaque text fields, there isn't even a split between a package name and the version range.

On the other hand, in cabal-like envelope there simply aren't any built-in "types": no lists, no numbers, no booleans. As a actual file format designer you need to choose how to represent them, allowing you to pick the format best suited for the domain. For example, in .cabal files we don't need to write versions in quotes, even if we have single digit versions!

For the purpose of automatic "exact-print" editing, it would be best if envelope format supported as much of needed structure as possible (e.g. there would be package name and version range split). For example in Cargo

[dependencies]
time = "0.1.12"

the separation is there.

OTOH, there is a gotcha:

Leaving off the caret is a simplified equivalent syntax to using caret requirements. While caret requirements are the default, it is recommended to use the simplified syntax when possible.

I'm quite sure that a lot of ad-hoc tools work only with simplified syntax.

Having simple envelope format is then probably the second best. If some file-format specific parsing has to be written anyway (e.g. to parse version ranges), dealing with a bit more complex stuff (like lists in .cabal build-depends) shouldn't be considerably more effort.

Greibach lexing-parsing

In formal language theory, a context-free grammar is in Greibach normal form (GNF) if the right-hand sides of all production rules start with a terminal symbol, optionally followed by some variables:

A → xBC
A → yDE

This suggests a representation for parsing procedure output, which looks like token stream (can be lazily constructed and consumed), but does represent a complete parse result, not just the result of lexing.

The idea is to have a continuation parameter for each production, A may start with X (A1 constructor) and then continue with B, which continues with C and then eventually with k.

data A e k
  = A1 X (B e (C e k))
  | A2 Y (D e (E e k))
  | A_Err e

Additionally have an error constructor so the possible parse errors are embedded somewhere later in t he stream. So there is A = ... | A_Err, B = ... | B_Err etc.

This may sound complicated, but it isn't. For simple grammars, the tokens stream type isn't that complicated. See for example aeson's Tokens. For JSON value, the Tokens looks almost like the Value type, but it does preserve more of the grammar. For example, the key order in maps is "as written", etc. This is sometimes important distinction: do you want a syntax representation or a value representation.

A cabal-like envelope format is also a simple grammar, which can be parsed into similar token stream. In cabal-fields it looks like

data AnnByteString ann = ABS ann {-# UNPACK #-} !ByteString
  deriving (Show, Eq, Functor, Foldable, Traversable)

data Tokens ann k e
    = TkSection !(AnnByteString ann) !(AnnByteString ann) (Tokens ann (Tokens ann k e) e)
    | TkField !(AnnByteString ann) !ann (TkFieldLines ann (Tokens ann k e) e)
    | TkComment !(AnnByteString ann) (Tokens ann k e)
    | TkEnd k
    | TkErr e
  deriving (Show, Eq)

data TkFieldLines ann k e
    = TkFieldLine !(AnnByteString ann) (TkFieldLines ann k e)
    | TkFieldComment !(AnnByteString ann) (TkFieldLines ann k e)
    | TkFieldEnd k
    | TkFieldErr e
  deriving (Show, Eq, Functor, Foldable, Traversable)

compare this to the Field type in Cabal-syntax; not considerably more complicated.

A benefit of Greibach-parsing is that it's relatively easy to write FFI-able parsers in C. We don't need to create AST, we can have lexer-like interface, leaving the handling of AST creation to the host language. The parser implementation can be embedded as easily embedded into e.g. Haskell or Python.

Cabal and braces

I must admit I like cabal-like format a lot. It's simplicity and free-formness make it good fit for almost any kind of configuration.

But there is a feature that I very much dislike.

While .cabal files are perceived to have white-space layout, there's actually a curly-braces option. With curly-braces you can write the whole .cabal file on a single line!

If you look (but I don't recommend) into grammar for cabal envelope, the handling of curly-braces, and especially how it interacts with whitespace layout, you'll see some horrific stuff.

You can write

test-suite hkd-example
  default-language: Haskell2010
  type: { exitcode-stdio-1.0 } main-is:HKD.hs 
  hs-source-dirs:   test
  build-depends:
      base
    , some

but I kindly ask you, please don't. :P

In short, for a feature used (or known) as little (but surprisingly a lot, 2.5% of Hackage; more than packages using tabs!), it adds quite a lot of complexity! And I'd argue that the syntax is not natural. And if it wasn't there, it wouldn't be added today.

So for now, I simply don't support it. Cabal-syntax must support all the stuff and warts, cabal-fields doesn't.

Cabal and section arguments

Another gotcha in cabal envelope format is that while the field contents are opaque, the section arguments (e.g. the test-suite name, or expression in if) is actually lexed. It's non an opaque string, i.e. cannot be arbitrary.

The only case where it makes a difference i can think of top my head, is to allow end-of-line comments. E.g. you can today write (and some did / do on Hackage):

flag tagged -- toggle me
  default: True
  manual: True

but I wouldn't recommend.

This is the only case where you can have a comment on otherwise non-whitespace line. E.g. if you write

  build-depends: base <5 -- i feel lucky

that won't work, the -- i feel lucky will be considered as part of the field content.

Doing it so makes the envelope format simpler: there are no escaping on the envelope level. If you escape something in e.g. description: field, it's handled by only by haddock. That avoids double escaping head-aches.

So cabal-fields treats section arguments as an opaque text. If you have a end-of-line comment on that line, it will be included.

C interface

The cabal-fields library was first prototyped in Haskell and has safe interface. However, C doesn't have sum types, nor polymorphic recursion nor many safety features at all. So the C version looks an ordinary lexer interface would. But there is a guarantee that only valid cabal-like files will be recognised, so the token stream will be well-formed; or an error token will be returned.

Python interface

I tested the pure Haskell version against Haskell-using-C-FFI version. They behave the same (against the most of Hackage).

The goal however was to parse .cabal files with Python. People do complain that they cannot modify the .cabal files with Python. Why I don't understand why you'd use Python, if you can use Haskell, but not you "can" use Python too.

The cabalfields-demo.py by default parsers and exact-prints the input files:

% python3 cabalfields-demo.py ../cabal-fields/cabal-fields.cabal 
../cabal-fields/cabal-fields.cabal
??? same: True
cabal-version: 2.4
name:          cabal-fields
version:       0.1
synopsis:      An alternative parser for .cabal like files
description:   An alternative parser for @.cabal@ like files.
...

with intermediate types which look like:

class Field:
    def __init__(self, name, name_pos, colon_pos, contents):
        self.name = name
        self.name_pos = name_pos
        self.colon_pos = colon_pos
        self.contents = contents

class Section:
    def __init__(self, name, name_pos, args, contents):
        self.name = name
        self.name_pos = name_pos
        self.args = args
        self.contents = contents

class FieldLine:
    def __init__(self, contents, pos):
        self.contents = contents
        self.pos = pos

class Comment:
    def __init__(self, contents, pos):
        self.contents = contents
        self.pos = pos

I haven't yet added any modification or consistency functionality.

It would be simpler to edit the structure if instead of absolute positions, there would be differences; and the pretty-printer would check that differences are consistent (i.e. there are needed newlines, enough indentation etc). That shouldn't be too difficult of an exercise to do. It might be easier to do on Haskell version first (types do help).

Perfectly, the C library would also contain a builder. But it needs a prototype first.

Also it's easier to write parsers in C, we don't need to think of memory allocation: the tokens returned are splices of the input byte array. Inn printing we need to have some kind of a builder abstraction: we would like to have an interface which can be used to produce both continuous strict byte-array for Python (using custom allocators), but also lazy ByteString in Haskell.

Conclusion

cabal-fields is a library for parsing .cabal like files. It is using Greibach lexing-parsing approach. It doesn't support curly braces, and slightly differs in how it handles section arguments. There is also a C implementation. With a Python module using it. And small demo of exact-printing .cabal like files from Python.

Safe coercions in GHC are a very powerful feature. However, they are not perfect; and already many years ago I was also thinking about how we could make them more expressive.

In particular such things like "higher-order roles" have been buzzing. For the record, I don't think Proposal #233 is great; but because that proposal is almost four years old, I don't remember why; nor I have tangible counter-proposal either.

So I try to recover my thoughts.

I like to build small prototypes; and I wanted to build a small language with zero-cost coercions.

The first approach, I present here, doesn't work.

While it allows model coercions, and very powerful ones, these coercions are not zero-cost as we will see. For language like GHC Haskell where being zero-cost is non-negotiable requirement, this simple approach doesn't work.

The small "formalisation" is in Agda file https://gist.github.com/phadej/5cf29d6120cd27eb3330bc1eb8a5cfcc

Syntax

We start by defining syntax. Our language is "simple": there are types

A, B = A -> B     -- function type, "arrow"

coercions

co = refl A        -- reflexive coercion
   | sym co        -- symmetric coercions
   | arr co₁ co₂   -- coercion of arrows built from codomain and domain
                   -- type coercions

and terms

f, t, s = x         -- variable
        | f t       -- application
        | λ x . t   -- lambda abstraction
        | t ▹ co    -- cast

Obviously we'd add more stuff (in particular, I'm interested in expanding coercion syntax), but these are enough to illustrate the problem.

Because the language is simple (i.e. not dependent), we can define typing rules and small step semantics independently.

Typing

There is nothing particularly surprising in typing rules.

We'll need a "well-typed coercion" rules too though, but these are also very straigh-forward

Coercion Typing:  Δ ⊢ co : A ≡ B

------------------
Δ ⊢ refl A : A ≡ A

Δ ⊢ co : A ≡ B
------------------
Δ ⊢ sym co : B ≡ A

Δ ⊢ co₁ : C ≡ A
Δ ⊢ co₂ : D ≡ B
-------------------------------------
Δ ⊢ arr co₁ co₂ : (C -> D) ≡ (A -> B)

Terms typing rules are using two contexts, for term and coercion variables (GHC has them in one, but that is unhygienic, there's a GHC issue about that). The rules for variables, applications and lambda abstractions are as usual, the only new is the typing of the cast:

Term Typing: Γ; Δ ⊢ t : A

Γ; Δ ⊢ t : A 
   Δ ⊢ co : A ≡ B
-------------------------
Γ; Δ ⊢ t ▹ co : B 

So far everything is good.

But when playing with coercions, it's important to specify the reduction rules too. Ultimately it would be great to show that we could erase coercions either before or after reduction, and in either way we'll get the same result. So let's try to specify some reduction rules.

Reduction rules

Probably the simplest approach to reduction rules is to try to inherit most reduction rules from the system without coercions; and consider coercions and casts as another "type" and "elimination form".

An elimination of refl would compute trivially:

t ▹ refl A ~~> t

This is good.

But what to do when cast's coercion is headed by arr?

t ▹ arr co₁ co₂ ~~> ???

One "easy" solution is to eta-expand t, and split the coercion:

t ▹ arr co₁ co₂ ~~> λ x . t (x ▹ sym co₁) ▹ co₂

We cast an argument before applying it to the function, and then cast the result. This way the reduction is type preserving.

But this approach is not zero-cost.

We could not erase coercions completely, we'll still need some indicator that there were an arrow coercion, so we'll remember to eta-expand:

t ▹ ??? ~~> λ x . t x

Conclusion

Treating coercions as another type constructor with cast operation being its elimination form may be a good first idea, but is not good enough. We won't be able to completely erase such coercions.

Another idea is to complicate the system a bit. We could "delay" coercion elimination until the result is scrutinised by another elimination form, e.g. in application case:

(t ▹ arr co₁ co₂) s ~~> t (s ▹ sym co₁) ▹ co₂ 

And that is the approach taken in Safe Zero-cost Coercions for Haskell, you'll need to look into JFP version of the paper, as that one has appendices.

(We do not have space to elaborate, but a key example is the use of nth in rule S_KPUSH, presented in the extended version of this paper.)

The rule S_Push looks some what like:

---------------------------------------------- S_Push
(t ▹ co) s ~~> t (s ▹ sym (nth₁ co)) ▹ nth₂ co

where we additionally have nth coercion constructor to decompose coercions.

Incidentally there was, technically is, a proposal to remove decomposition rule, but it's a wrong solution to the known problem. The problem and a proper solution was kind of already identified in the original paper

We could similarly imagine a lattice keyed by classes whose instance definitions are to be respected; with such a lattice, we could allow the coercion of Map Int v to Map Age v precisely when Int’s and Age’s Ord instances correspond.

The original paper also identified the need for higher-order roles. And also identified that

This means that Monad instances could be defined only for types that expect a representational parameter.

which I argue should be already required for Functor (and traverseBia hack with unlawful Mag would still work if GHC had unboxed representational coercions, i.e. GADTs with baked-in representational (not only nominal) coercions).

There also the mention of unidirectional Coercible, which people asked about later and recently:

Such uni-directional version of Coercible amounts to explicit inclusive subtyping and is more complicated than our current symmetric system.

It is fascinating that authors were able to predict the relevant future work so well. And I'm thankful that GHC got Coercible implemented even it was already known to not be perfect. It's useful nevertheless. But I'm sad that there haven't been any results of future work since.

Recently I came up with a criteria for a good warning to have in a compiler:

If compiler makes a choice, or has to deal with some complication, it may well tell about that.

That made me think about warnings I implemented into GHC over the years. They are fine.

Let us first understand the criteria better. It is better explained by an example which triggers few warnings:

foo :: Char
foo = let x = 'x' in
      let x = 'y' in x

First warning is -Wname-shadowing:

Shadow.hs:3:11: warning: [-Wname-shadowing]
    This binding for ‘x’ shadows the existing binding
      bound at Shadow.hs:2:11
  |
3 |       let x = 'y' in x
  |           ^

When resolving names (i.e. figuring out what textual identifiers refer to) compilers have a choice what to do with duplicate names. The usual choice is to pick the closest reference, shadowing others. But it's not the only choice, and not the only choice GHC does in similar-ish situations. e.g. module's top-level definition do not shadow imports; instead an ambiguous name error is reported. Also \ x x -> x is rejected (treated as a non-linear pattern), but \x -> \x -> x is accepted (two separate patterns, inner one shadows). So, in a way, -Wname-shadowing reminds us what GHC does.

Another warning in the example is -Wunused-binds:

Shadow.hs:2:11: warning: [-Wunused-local-binds]
    Defined but not used: ‘x’
  |
2 | foo = let x = 'x' in
  |           ^

This a kind of warning that compiler might figure out in the optimisation passes (I'm not sure if GHC always tracks usage, but IIRC GCC had some warnings triggered only when optimisations are on). When doing usage analysis, compiler may figure out that some bindings are unused, so it doesn't need to generate code for them. At the same time it may warn the user.

More examples

Let go through few of the numerous warnings GHC can emit.

-Woverflowed-literals causes a warning to be emitted if a literal will overflow. It's not strictly a compiler choice, but a choice nevertheless in base's fromInteger implementations. For most types ¹ the fromInteger is a total function with rollover behavior: 300 :: Word8 is 44 :: Word8. It could been chosen to not be total too, and IMO that would been ok if fromInteger were used only for desugaring literals.

-Wderiving-defaults: Causes a warning when both DeriveAnyClass and GeneralizedNewtypeDeriving are enabled and no explicit deriving strategy is in use. This a great example of a choice compiler makes. I actually don't remember which method GHC picks then, so it's good that compiler reminds us that it is good idea to be explicit (using DerivingStrategies).

-Wincomplete-patterns warns about places where a pattern-match might fail at runtime. This a complication compiler has to deal with. Compiler needs to generate some code to make all pattern matches complete. An easy way would been to always implicitly default cases to all pattern matches, but that would have performance implications, so GHC checks pattern-match coverage, and as a side-product may report incomplete pattern matches (or -Winaccesible-code) ².

-Wmissing-fields warns you whenever the construction of a labelled field constructor isn’t complete, missing initialisers for one or more fields. Here compiler needs to fill the missing fields with something, so it warns when it does.

-Worphans gets an honorary mention. Orphans cause so much incidental complexity inside the compiler, that I'd argue that -Worphans should be enabled by default (and not only in -Wall).

Bad warnings

-Wmissing-import-lists warns if you use an unqualified import declaration that does not explicitly list the entities brought into scope. I don't think that there are any complications or choices compiler needs to deal with, therefore I think this warning should been left for style checkers. (I very rarely have import lists for modules from the same package or even project; and this is mostly a style&convenience choice).

-Wprepositive-qualified-module is even more of an arbitrary style check. With -Wmissing-import-lists it is generally accepted that explicit import lists are better for compatibility (and for GHCs recompilation avoidance). Whether you place qualified before or after the module name is a style choice. I think this warning shouldn't exist in GHC. (For the opposite you'd need a style checker to warn if ImportQualifiedPost is enabled anywhere).

Note, while -Wtabs is also mostly a style issue, but the compiler has to make a choice how to deal with them. Whether to always convert tabs to 8 spaces, convert to next 8 spaces boundary, require indentation to be exactly the same spaces&tabs combination. All choices are sane (and I don't know which one GHC makes), so a warning to avoid tabs is justified.

Compatibility warnings

Compatibility warnings are usually good also according to my criteria. Often it is the case that there is an old and a new way of doing things. Old way is going to be removed, but before removing it, it is deprecated.

-Wsemigroup warned about Monoid instances without Semigroup instances. (A warning which you shouldn't be able to trigger with recent GHCs). Here we could not switch to new hierarchy immediately without breaking some code, but we could check whether the preconditions are met for awhile.

-Wtype-equality-out-of-scope is somewhat similar. For now, there is some compatibility code in GHC, and GHC warns when that fallback code path is triggered.

My warnings

One of the warning I added is -Wmissing-kind-signatures. For long time GHC didn't have a way to specify kind signatures until StandaloneKindSignatures were added in GHC-8.10. Without kind signatures GHC must infer kind of a data type or type family declaration. With kind signature it could just check against given kind (which is a technically a lot easier). So while the warning isn't actually implemented so, it could be triggered when GHC notices it needs to infer a kind of a definition. In the implementation the warning is raised after the type-checking phase, so the warning can include the inferred kind. However, we can argue that when inference fails, GHC could also mention that the kind signature was missing. Adding a kind signature often results in better kind errors (c.f. adding a type signature often results in a better type error when something is wrong).

The -Wmissing-poly-kind-signatures warning seems like a simple restriction of above, but it's not exactly true. There is another problem GHC deals with. When GHC infers a kind, there might be unsolved meta-kind variables left, and GHC has to do something to them. With PolyKinds extension on, GHC generalises the kind. For example when inferring a kind of Proxy as in

data Proxy a = Proxy

GHC infers that the kind is k -> Type for some k and with PolyKinds it generalises it to type Proxy :: forall {k}. k -> Type. Another option, which GHC also may do (and does when PolyKinds are not enabled) is to default kinds to Type, i.e. type Proxy :: Type -> Type. There is no warning for kind defaulting, but arguable there should be as defaulted kinds may be wrong. (Haskell98 and Haskell2010 don't have a way to specify kind signatures; that is clear design deficiency; which was first resolved by KindSignatures and finally more elegantly by StandaloneKindSignatures).

There is defaulting for type variables, and (in some cases) GHC warns about them. You probably have seen Defaulting the type variable ‘a0’ to type ‘Integer’ warnings caused by -Wtype-defaults. Adding -Wkind-defaults to GHC makes sense, even only for uniformity between (types of) terms and types; or arguably nowadays it is a sign that you should consider enabling PolyKinds in that module.

About errors

The warning criteria also made me think about the following: the error hints are by necessity imprecise. If compiler knew exactly how to fix an issue, maybe it should just fix it and instead only raise a warning.

GHC has few of such errors. For example when using a syntax guarded by an extension. It can be argued (and IIRC was recently argued in discussions around GHC language editions) that another design approach would be simply accept new syntax, but just warn about it. The current design approach where extensions are "feature flags" providing some forward and backward compatibility is also defendable.

Conversely, if there is a case where compiler kind-of-knows what the issue is, but the language is not powerful enough for compiler to fix the problem on its own, the only solution is to raise an error. Well, there is another: (find a way to) extend the language to be more expressive, so compiler could deal with the currently erroneous case. Easier said than done, but in my opinion worth trying.

An example of above would be -Wmissing-binds . Currently writing a type signature without a corresponding binding is a hard error. But compiler could as well fill it in with a dummy one, That would complement -Wmissing-methods and -Wmissing-fields. Similarly for types, a standalone kind signature tells the compiler already a lot about the type even without an actual definition: the rest of the module can treat it as an opaque type.

Another example is briefly mentioned making module-top-level definitions shadow imports. That would make adding new exports (e.g. to implicitly imported Prelude) less affecting. While we are on topic of names, GHC could also report early when imported modules have ambiguous definitions, e.g.

import qualified Data.Text.Lazy as Lazy
import qualified Data.ByteString.Lazy as Lazy

doesn't trigger any warnings. But if you try to use Lazy.unpack you get an ambiguous occurrence error. GHC already deals with the complications of ambiguous names, it could as well have an option to report them early.

Conclusion

If compiler makes a choice, or has to deal with some complication, it may well tell about that.

Seems like a good criteria for a good compiler warning. As far as I can tell most warnings in GHC pass it; but I found few "bad" ones too. And also identified at least one warning-worthy case GHC doesn't warn about.

inspection-testing was created over five years ago. You may want to glance over Joachim Breitner A promise checked is a promise kept: inspection testing) Haskell Symposium paper introducing it.

Already in 2018 I thought it's a fine tool, but it's more geared towards /library/ writers. They can check on (some) examples that the promises they make about the libraries they write work at least on some examples.

What we cannot do with current inspection-testing is check that the actual "real-life" use of the library works as intended.

Luckily, relatively recently, GHC got a feature to include all Core bindings in the interface files. While the original motivation is different (to make Template Haskell run fast), the -fwrite-if-simplified-core enables us to inspect (as in inspection testing) the "production" Core (not the test examples).

The cabal-core-inspection is a very quick & dirty proof-of-concept of this idea.

Let me illustrate this with two examples.

In neither example I need to do any test setup, other than configuring cabal-core-inspection (though configuration is now hardcoded). Compare that to configuring e.g. HLint (HLint has user definable rules, and these are actually powerful tool). In fact, cabal-core-inspection is nothing more than a linter for Core.

countChars

First example is countChars as in Haskell Symposium Paper.

countChars :: ByteString -> Int
countChars = T.length . T.toUpper . TE.decodeUtf8

The promise is (actually: was) that no intermediate Text values are created.

As far as I know, we cannot use inspection-testing in its current form to check anything about non-local bindings, so if countChars is defined in an application, we would need to duplicate its definition in the test-suite to inspect it. That is not great.

With Core inspection, we can look at the actual Core of the module (as it is in the compiler interface file).

The prototype doesn't have any configuration, but if we imagine it has we could ask it to check that Example.countChars should not contain type Text. The prototype prints

Text value created with decodeUtf8With1 in countChars

So that's not the case. The intermediate Text value is created. In fact, nowadays text doesn't promise that toUpper fuses with anything.

A nice thing about cabal-core-inspection that (in theory) it could check any definition in any module as long as it's compiled with -fwrite-if-simplified-core. So we could check things for our friends, if we care about something specific.

no Generics

Second example is about GHC.Generics. I use a simple generic equality, but this could apply to any GHC.Generics based deriving. (You should rather use deriving stock Eq, but generic equality is a simplest example which I remembered for now).

The generic equality might be defined in a library. And library author may actually have tested it with inspection-testing. But does it work on our type?

If we have

data T where
    T1 :: Int -> Char -> T
    T2 :: Bool -> Double -> T
  deriving Generic

instance Eq T where
    (==) = genericEq

it does. The cabal-core-inspection doesn't complain.

But if we add a third constructor

data T where
    T1 :: Int -> Char -> T
    T2 :: Bool -> Double -> T
    T3 :: ByteString -> T.Text -> T

cabal-core-inspection barfs:

Found L1 from GHC.Generics
Found :*: from GHC.Generics
Found R1 from GHC.Generics

The T becomes too large for GHC to want inline all the generics stuff.

It won't be fair to blame the library author, for example for

data T where
    T1 :: Int -> T
    T2 :: Bool -> T
    T3 :: Char -> T
    T4 :: Double -> T
  deriving Generic

generic equality still optimises well, and doesn't have any traces of GHC.Generics. We may actually need to (and may be adviced to) tune some GHC optimisation parameters. But we need a way to check whether they are enough. inspection-testing doesn't help, but a proper version of core inspection would be perfect for that task.

Conclusion

The -fwrite-if-simplified-core enables us to automate inspection of actual Core. That is a huge win. The cabal-core-inspection is just a proof-of-concept, and I might try to make it into a real thing, but right now I don't have a real use case for it.

I'm also worried about Note [Interface File with Core: Sharing RHSs] in GHC. It says

In order to avoid duplicating definitions for bindings which already have unfoldings we do some minor headstands to avoid serialising the RHS of a definition if it has *any* unfolding.

• Only global things have unfoldings, because local things have had their unfoldings stripped.
• For any global thing which has an unstable unfolding, we just use that.

Currently this optimisation is disabled, so cabal-core-inspection works, but if it's enabled as is; then INLINEd bindings won't have their simplified unfoldings preserved (but rather only "inline-RHS"), and that would destroy Core inspection possibility.

But until then, cabal-core-inspection idea works.

In programming languages with sophisticated type systems we easily run into inconvenience of providing many (often type) arguments explicitly. Let's take a simple map function as an example:

map :: forall a b. (a -> b) -> List a -> List b

If we had to always explicitly provide map's arguments, write something like

ys = map @Char @Char toLower xs

we would immediately give up on types, and switch to use some dynamically typed programming language. It wouldn't be fun to state "the obvious" all the time.

Fortunately we know a way (unification) which can be used to infer many such argument. Therefore we can write

ys = map toLower xs

and the type arguments will be inferred by compiler. However we usually are able to be explicit if we want or need to be, e.g. with TypeApplications in GHC Haskell.

Beyond Hindley-Milner

Conor McBride calls a following phenomenon "Milner's Coincidence":

The Hindley-Milner type system achieves the truly awesome coincidence of four distinct distinctions

• terms vs types
• explicitly written things vs implicitly written things
• presence at run-time vs erasure before run-time
• non-dependent abstraction vs dependent quantification

We’re used to writing terms and leaving types to be inferred. . . and then erased. We’re used to quantifying over type variables with the corresponding type abstraction and application happening silently and statically.

GHC Haskell type-system has been long far more expressive than vanilla Hindley-Milner, and the four distrinctions are already misaligned.

GHC developers are filling the cracks: For example we'll soon ¹ get a forall a -> (with an arrow, not a dot) quantifier, which is erased (irrelevant), explicit (visible) dependent quantification. Later we'll get foreach a. and foreach a -> which are retained (i.e. not-erased, relevant) implicit/explicit dependent quantification.

(Agda also has "different" quantifiers: explicit (x : A) -> ... and implicit {y : B} -> ... dependent quantifiers, and erased variants look like (@0 x : A) -> ... and {@0 y : B} -> ....)

In Haskell, if we have a term with implicit quantifier (foo :: forall a. ...), we can use TypeApplications syntax to apply the argument explicitly:

bar = foo @Int

If the quantifier is explicit, we'll (eventually) write just

bar = foo Int

or

bar = foo (type Int)

for now.

Inferred type variables

That all is great, but consider we define a kind-polymorphic² type like

type ProxyE :: forall k. k -> Type
data ProxyE a = MkProxyE

then when used at type level, forall behaves as previously, constructors

ghci> :kind ProxyE Int
ProxyE Int :: Type

ghci> :kind ProxyE @Type Int
ProxyE @Type Int :: Type

The type of constructor MkProxyE is

ghci> :type ProxyE
ProxyE :: forall k (a :: k). ProxyE @k a

So if we want to create a term of type Proxy Int, we need to provide both k and a arguments:

ghci> :type ProxyE @Type @Int
ProxyE @Type @Int :: ProxyE @(Type) Int

we could also jump over k:

ghci> :type MkProxyE @_ @Int
MkProxyE @_ @Int :: ProxyE @(*) Int

The above skipping over arguments is not convenient, luckily GHC has a feature, created for other needs, which we can (ab)use here. There are inferred variables (though the better name would be "very hidden"), these are arguments for which TypeApplication doesn't apply:

type Proxy :: forall {k}. k -> Type
data Proxy a = MkProxy

This is the way Proxy is defined in base (but I renamed the constructor to avoid name ambiguity)

And while GHCi prints

ghci> :type MkProxy @Int
MkProxy @Int :: Proxy @{Type} Int

the @{A} syntax is not valid Haskell, so we cannot explicitly apply inferred variables. Neither we can in types:

ghci> :kind! Proxy @{Type}

<interactive>:1:10: error: parse error on input ‘Type’

I think this is plainly wrong, we should be able to apply these "inferred" arguments too.

The counterargument is that, inferred variables weren't meant to be "more implicit" variables. As GHC manual explains, inferred variables are a solution to TypeApplications with inferred types. We need to know the order of variables to be able to apply them; but especially in presence of type-class constraints the order is arbitrary.

I'm not convinced, I think that ability to be fully explicit is way more important than a chance to write brittle code.

One solution, which I think would work, is simply to not generalise. This is controversial proposal, but as GHC Haskell is moving towards having fancier type system, something needs to be sacrificed. (MonoLocalBinds is for local bindings, but I'd argue that should be for all bindings, not only local).

The challenge has been that library writes may not been aware of TypeApplications, but today they have no choice. Changing from foo :: forall a b. ... to foo :: forall b a. ... may break some code (even though PVP doesn't explicitly write that down, that should be common sense).

So in the GHC manual example

f :: (Eq b, Eq a) => a -> b -> Bool
f x y = (x == x) && (y == y)

g x y = (x == x) && (y == y)

the g would fail to type-check because there are unsolved type-variables. One way to think about this is that GHC would refuse to pick an order of variables. GHC could still generalise if there are no dictionary arguments, but on the other hand I don't think it would help much. It might help more if GHC wouldn't specialise as much, then

h = f

would type-check.

This might sound like we would need to write much many type signatures. I don't think that is true: it's already a best practice to write type signatures for type level bindings, and for local bindings we would mostly need to give signatures to function bindings.

This proposal subsumes monomorphism restriction, recall that without type defaulting:

-- turn off defaulting
default ()
fooLen = genericLength "foo"

will fail to compile with

Ambiguous type variable ‘i0’ arising from a use of ‘genericLength’
prevents the constraint ‘(Num i0)’ from being solved.

error. With NoMonomophismRestriction we have

ghci> :t fooLen
fooLen :: Num i => i

Another, a lot simpler option, is to simply remember whether the symbols' type was inferred, and issue a warning if TypeApplications is used with such symbol in application head. So if user writes

... (g @Int @Char ...)

GHC would warn that g has inferred type, and the TypeApplications with g are brittle. The solution is to give g a type signature. This warning could be issued early in a pipeline (maybe already in renamer), so it would explain further (possibly cryptic) type errors.

Let me summarise the above: If we could apply inferred variables, i.e. use curly brace application syntax, we would have complete explicit forall a ->, implicit forall a. and more implicit forall {a}. dependent quantifiers. Currently the forall {a}. quantifier is incomplete: we can abstract, but we cannot apply. We'll also need some alternative solution to TypeApplicaitons and inferred types. We should be able to bind these variables explicitly in lambda abstractions as well: \ a ->, \ @a -> and \ @{a} -> respectively (see TypeAbstractions).

Alternatives

The three level explicit/implicit/impliciter arguments may feel complicated. Doesn't other languages have similar problems, how they solve them?

As far as I'm aware Agda and Coq resolve this problem by supporting applying implicit arguments by name:

-- using indices instead of parameters,
-- to make constructor behave as in Haskell
data Proxy : {k : Set} (a : k) -> Set1 where
  MkProxy : {k : Set} {a : k} -> Proxy a

t = MkProxy {a = true}

Just adding named arguments to Haskell would be a bad move. It would add another way where a subtle and well-meaning change in the library could break downstream. For example unifying the naming scheme of type-variables in the libraries, so they are always Map k v and not Map k a sometimes, as it is in containers which uses both variable namings.

We could require library authors to explicitly declare that bindings in a module can be applied by name (i.e. that they have thought about the names, and recognise that changing them will be breaking change). You would still be able to always explicitly apply implicit arguments, but sometimes you won't be able to use more convenient named syntax.

It is fair to require library authors to make adjustments so that (numerous) library users would be able to use a new language feature with that library. In a healthy ecosystem that shouldn't be a problem. Specifically it is extra fair, if the alternative is to make feature less great, as then people might not use it at all.

Infinite level of implicitness

Another idea is to embrace implicit, more implicit and even more implicit arguments. Agda has two levels: explicit and implicit, GHC Haskell has two and a half, why stop there?

If we could start fresh, we could pick Agda's function application syntax and have

funE arg    -- explicit application
funI {arg}  -- explicit application of implicit argument

but additionally we could add

funJ {{arg}}    -- explicit application of implicit² argument
funK {{{arg}}}  -- explicit application of implicit³ argument
...             -- and so on

With unlimited levels of implicitness we could define Proxy as

type Proxy :: forall {k} -> k -> Type
data Proxy a where
    MkProxy :: forall {{k}} -> {a :: k} -> Proxy a

and use it as MkProxy, MkProxy {Int} or MkProxy {{Type}} {Int} :: Proxy Int. Unlimited possibilities.

For what it is worth, the implementation should be even simpler than of named arguments.

But I'd be quite happy already if GHC Haskell had a way to explicitly apply any function arguments, be it three levels (ordinary, @arg and @{arg}) of explicitness, many or just two; and figured another way to tackle TypeApplications with inferred types.

Implementation

I wish there were an early exit functionality in the ST monad. This need comes time to time when writing imperative algorithms in Haskell.

It's very likely there is a functional version of an algorithm, but it might be that ST-version is just simply faster, e.g. by avoiding allocations (as allocating even short lived garbage is not free).

But there are no early exit in the ST monad.

Recent GHC added delimited continuations. The TL;DR is that delimited continuations is somewhat like goto:

• newPromptTag# creates a label (tag)
• prompt# brackets the computation
• control# kind of jumps (goes to) the end of enclosing prompt bracket, and continues from there.

So let's use this functionality to implement a version of ST which has an early exit. It turns out to be quite simple.

The ST monad is define like:

newtype ST s a = ST (State# s -> (# State# s, a #)

and we change it by adding an additional prompt tag argument:

newtype EST e s a = EST
    { unEST :: forall r. PromptTag# (Either e r)
            -> State# s -> (# State# s, a #) 
    }

(Why forall r.? We'll see soon).

It's easy to lift normal ST computations into EST ones:

liftST :: ST s a -> EST e s a
liftST (ST f) = EST (\_ -> f)

so EST is a generalisation of ST, good.

Now we need a way to run EST computations, and also a way to early exit in them.

The early exit is the simpler one. Given that tag prompt brackets the whole computation, we simply jump to the end with Left e. We ignore the captured continuation, we have no use for it.

earlyExitEST :: e -> EST e s any
earlyExitEST e = EST (\tag -> control0## tag (\_k s -> (# s, Left e #)))

Now, the job for runEST is to create the tag and prompt the computation:

runEST :: forall e a. (forall s. EST e s a) -> Either e a
runEST (EST f) = runRW#
    -- create tag
    (\s0 -> case newPromptTag# s0 of {
    -- prompt
    (# s1, tag #) -> case prompt# tag
         -- run the `f` inside prompt,
         -- and once we get to the end return `Right` value
         (\s2 -> case f tag s2 of (# s3, a #) -> (# s3, Right a #)) s1 of {
    (# _, a #) -> a }})

runRW# and forgetting the state at the end is the same as in runST, for comparison:

runST :: (forall s. ST s a) -> a
runST (ST st_rep) = case runRW# st_rep of (# _, a #) -> a
-- See Note [runRW magic] in GHC.CoreToStg.Prep

With all the pieces in place, we can run few simple examples:

-- | >>> ex1
-- Left 'x'
ex1 :: Either Char Bool
ex1 = runEST $ earlyExitEST 'x'

-- | >>> ex2
-- Right True
ex2 :: Either Char Bool
ex2 = runEST (return True)

Comments & wrinkles

Early exit is one of the simplest "effect" you can implement with delimited continuations. This is the throwing part of the exceptions, with only top-level exception handler. It's a nice exercise (and a brain twister) to implement catch blocks.

One wrinkle in this implementation is the control0## (not control0#) function I used. The delimited continuations primops are made to work only with RealWorld, not arbitrary State# tokens.

I think this is unnecessary specialization GHC issue #24165, I was advice to simply use unsafeIOToST, so I did:

control0##
    :: PromptTag# a
    -> (((State# s -> (# State# s, b #)) -> State# s -> (# State# s, a #))
                                         -> State# s -> (# State# s, a #))
    -> State# s -> (# State# s, b #)
control0## = unsafeCoerce# control0#

This still feels silly, especially realizing that the (only) example in the delimited continuations proposal goes like

type role CC nominal representational
newtype CC ans a = CC (State# RealWorld -> (# State# RealWorld, a #))
  deriving (Functor, Applicative, Monad) via IO

runCC :: (forall ans. CC ans a) -> a
runCC (CC m) = case runRW# m of (# _, a #) -> a

but if you look at that, it's just a ST monad done weirdly:

newtype ST s a = ST (State# RealWorld -> (# State# RealWorld, a #))
-- not using `s` argument !?

There might be a good reason why CC should be done like that (other than than primops are RealWorld specific), but the proposal doesn't explain that difference. To me having phantom ans instead of using nominally it as in ST is suspicious.

Conclusion

Delimited continutations are fun and could be very useful.

But surprisingly, at the moment of writing I cannot find any package on Hackage using them for anything! Search for newPromptTag returns only false positives (ghc-lib etc) right now. I wonder why they are unused?

Please try them out!

Qualified do-notation, QualifiedDo, is a nice syntactical extension in GHC. Probably the best its property is that it changes semantics only locally, by using explicit "annotation": by qualifying the do keyword¹. This means that enabling the extension doesn't change meaning of other & existing code.

I'll give two examples of QualifiedDo applications.

First example: COMPLETE pattern synonyms

GHC had long had PatternSynonyms. One use case for pattern synonyms is to provide backward compatibility when data type constructors change: preserving old constructor names and arguments as a compatibility pattern synonym.

For example, we used to have data Solo = Solo a. Recently the constructor was renamed to MkSolo to avoid name punning. To not break all the code using Solo constructor there compatibility pattern synonym was added:

pattern Solo :: a -> Solo
pattern Solo x = MkSolo x
{-# COMPLETE Solo #-}

The COMPLETE pragma says that a pattern match using Solo pattern synonym is complete, so we wouldn't get incomplete pattern match warnings².

But COMPLETE support is (ironically) incomplete. If we have a do block like

broken :: Monad m => m (Solo a) -> m a
broken s = do
    Solo x <- s
    return x

the GHC will error because we don't have MonadFail instance (to desugar incomplete pattern match: Could not deduce (MonadFail m), that is GHC issue #15681). There are various workarounds, but I don't remember anyone mentioning QualifiedDo.

If we write a small helper module

module M ((>>=), (>>), fail) where

import Prelude ((>>=), (>>), Monad, String, error)
import GHC.Stack

fail :: (Monad m, HasCallStack) => String -> m a
fail = error

we can change broken into something which works:

import qualified M

works :: Monad m => m (Solo a) -> m a
works s = M.do
    Solo x <- s
    return x

Now if GHC needs to fail, it will simply error.

I hope that it's obvious that this is a band-aid: if you are relying on fail doing something useful (e.g. in Maybe), this will obviously break your program. But as QualifiedDo usage is explicitly annotated it's not a spooky action at the distance. And HasCallStack annotation should help you find the mistakes if any happen.

Second example: zero-overhead effects

At work I have been (adjacently) working with the code building on top of io-sim. TL;DR you write your code using (a lot of) type-classes, and then can either run your code in real IO (production) or in a simulator IOSim (for tests). But I'm getting slightly anxious thinking about having all I/O code being abstracted using type-classes making the true IO case potentially go slow. (This is mtl-like take on effect handling, but even effectful or something based on delimited continuations aren't zero-overhead: the overhead is there, just smaller).

What we truly want is a complete specialisation of effect-related type-classes, so there aren't any abstraction bits left when the use case is concrete (in mtl approach we can theoretically get there, but not in practice. In effectful or delimited-continuations a small cost is always there, but it doesn't rely that much on compiler optimising well).

Most likely, if your code isn't pushing both the I/O and CPU utilization at the same time, either approach will work ok. Compare that to data science done in Python: Python is a quite slow glue language, but it's combining bigger fast running "primitive" blocks. So if there is very little glue code, and the most work is done inside the abstracted primitives, the glue being tacky doesn't matter.

But can we do better?

In GHC we can do better using staging i.e. Typed Template Haskell (TTH). At first I was worried that TTH syntactic overhead will be off-putting until I remembered that QualifiedDo extension exists!

We can write code like:

import qualified SIO

example :: SIO.SIO i m => i FilePath -> m ()
example fn = SIO.do
  contents <- SIO.readFile fn
  SIO.putStr contents

that looks like normal Haskell. If we were forced to use >>= like operator explicitly, e.g. writing

example' :: SIO.SIO i m => i FilePath -> m ()
example' fn =
  SIO.readFile fn >>>= \contents ->
  SIO.putStr contents

it wouldn't be as nice.

The SIO type class has the part which looks almost like Monad, but not exactly:

class SIO i m | m -> i where
  (>>=)    :: m a -> (i a -> m b) -> m b

The "pure" values are wrapped inside type constructor i (for identity).

The readFile and putStr are also in the same type-class (could be different, doesn't really matter):

  readFile :: i FilePath -> m ByteString
  putStr   :: i ByteString -> m ()

We can have concrete instances, like IO (or actually IOSim) for tests:

instance SIO Identity IO where
  (>>=) :: forall a b. IO a -> (Identity a -> IO b) -> IO b
  (>>=) = coerce (bindIO @a @b)

  readFile = coerce BS.readFile
  putStr = coerce BS.putStr

But because we are liberated from the restricting shape of the Monad type class, we can have instance for CodeQ from template-haskell:

newtype CodeIO a = CodeIO { unCodeIO :: CodeQ (IO a) }

instance SIO CodeQ CodeIO where
  m >>= k     = CodeIO
    [|| bindIO $$(unCodeIO m) (\x -> $$(unCodeIO (k [|| x ||]))) ||]
  readFile fn = CodeIO [|| BS.readFile $$fn ||]
  putStr bs   = CodeIO [|| BS.putStr $$bs ||]

Then in our main production module we can splice the example in like

spliced :: FilePath -> IO ()
spliced fn = $$(SIO.unCodeIO $ SIO.do
    example [|| fn ||]
    example [|| fn ||])

and the generated code has no effect handling abstractions; in fact not even a Monad, as we used thenIO and bindIO building blocks:

spliced fn_a3kY =
    (GHC.Base.thenIO
       ((GHC.Base.bindIO (Data.ByteString.readFile fn_a3kY))
          (\ x_a3m2 -> Data.ByteString.putStr x_a3m2)))
      ((GHC.Base.bindIO (Data.ByteString.readFile fn_a3kY))
         (\ x_a3m3 -> Data.ByteString.putStr x_a3m3))

We have a precise control (but also a responsibility) to control the inlining of building blocks (i.e. if we want example let-bound first and then called twice, we must do that manually: power comes with responsibility). This is either a pro or con, depending on your POV. I think this is a pro if you go this far caring about the performance. If GHC Haskell had a type-class like mechanism with full monomorphisation guarantee, we'd would still like to to control inlining.

You may also worry that "wont staging generate a lot of code". Yes it will, but so would full monomorphisation (of templates in C++ or traits in Rust). It's a behaviour we arguably want, but it's GHC which may be worried and don't do too good job. With staging we could also do modular code-generation too, making layered type-class hierarchy, generating i.e. "pre-splicing" intermediate layers (layers like in three layer cake).

Conclusion

QualifiedDo is a neat GHC extension. We saw two more examples of its usage, where we want something like regular Monad desugaring, but which doesn't fit the Monad type-class. I also think we could have more of Qualified* syntactic extensions.