Skip to content

Instantly share code, notes, and snippets.

Last active April 1, 2022 19:06
  • Star 0 You must be signed in to star a gist
  • Fork 0 You must be signed in to fork a gist
Star You must be signed in to star a gist
What would you like to do?
Minimal reproduction for breaking Dhall's type system safety guarantees
-- This is a minimal reproducing example of a major escape hatch that
-- violate's Dhall type safety guarantees.
let -- The uninhabited type (isomorphic to `< >`, but this is more ergonomic to
-- use for this reproduction)
Void : Type = ∀(any : Type) → any
let -- We model type-level negation in the standard way as a function from a
-- given type to the uninhabited type. `Not a` is only inhabited if `a`
-- is uninhabited (i.e. isomorphic to `Void`)
Not : Type → Type = λ(p : Type) → p → Void
let -- The powerset of `X`
pow = λ(X : Kind) → X → Type
let -- If we define the following universe of over types:
U = ∀(X : Kind) → (pow (pow X) → X) → pow (pow X)
let -- … and then introduce the following mapping:
: pow (pow U) → U
= λ(t : pow (pow U))
→ λ(X : Kind)
→ λ(f : pow (pow X) → X)
→ λ(p : pow X)
→ t (λ(x : U) → p (f (x X f)))
in -- The soundness issue is that nobody can force you to use Dhall for your
-- project or, more generally, nobody can force you to use a language with
-- language security worth a damn. You can freely shoot yourself in the foot
-- using Bash or YAML or whatever
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment