You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
{{ message }}
This repository has been archived by the owner on Oct 18, 2021. It is now read-only.
According to Amulet's semantics, the following is a valid optimisation:
letx : t = e in
...
(* => *)letx : t = e inmatch 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"typevoid = |
external valbot : () -> 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.
The text was updated successfully, but these errors were encountered:
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.
Sign up for freeto subscribe to this conversation on GitHub.
Already have an account?
Sign in.
According to Amulet's semantics, the following is a valid optimisation:
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:After we have attributes, we could even mark functions as returning bottom, which would let us optimise uses of
(import "amulet/exception.ml").throw
.The text was updated successfully, but these errors were encountered: