amuletml / amulet

An ML-like functional programming language
https://amulet.works/
BSD 3-Clause "New" or "Revised" License
328 stars 16 forks source link

Let-of-bottom optimisation #216

Open plt-amy opened 5 years ago

plt-amy commented 5 years ago

According to Amulet's semantics, the following is a valid optimisation:

let x : t = e in
...
(* => *)
let x : t = e in
match x {}
(* iff t is empty *)

This is mostly a code size/compiler performance optimisation: the following program would get DCE'd to all but the call to bot, whereas currently it includes all of the IO/Exception machinery:

open import "prelude.ml"

type void = |
external val bot : () -> void = "error"

let _ =
  let x = bot ()
  put_line "can't get here"

After we have attributes, we could even mark functions as returning bottom, which would let us optimise uses of (import "amulet/exception.ml").throw.

plt-amy commented 5 years ago

I think the "empty type" is a good approximation but it might actually be a red herring. What we want is support for eliminating tails of bottoming computations generally (Amulet exceptions, compiler-generated error calls, infinite recursion, empty matches, "returning" an empty type, etc..), which is bloody hard to do in a well-typed way.