alligators.agda

{-# OPTIONS --no-import-sorts --erasure #-}
open import Agda.Primitive renaming (Set to Type)
open import Data.Nat
open import Data.Bool
open import Data.Product
open import Relation.Binary.PropositionalEquality

-- An element of `Remember a` is a witness that `a` exists at runtime.
data Remember {ℓ} {@0 A : Type ℓ} : (@0 a : A) → Type ℓ where
  instance remember : {a : A} → Remember a

Password = ℕ

-- A record type with a "password" that is erased at runtime.
-- This came up in a discussion about modelling Zig's "unmanaged" containers,
-- which must be passed their allocator for every potentially allocating
-- operation, instead of storing it as part of the data structure.
-- https://ziglang.org/download/0.14.0/release-notes.html#Embracing-Unmanaged-Style-Containers
record Data : Type where
  constructor mkData
  field
    @0 password : Password
    payload : ℕ

open Data

-- A function that manipulates Data, but requires the password to be
-- provided at runtime. This is a "verified" toy model of something like
-- Zig's std.ArrayList.append which requires the allocator used to
-- create the list to be given at runtime.
leak : (d : Data) → ⦃ Remember (d .password) ⦄ → Data
leak (mkData p w) ⦃ remember ⦄ = mkData p p -- p may be used at runtime

-- This fails to solve the argument to the remember instance, because
-- d .password is erased.
no-leak : Data → Data
no-leak d = {! leak d !}

-- This is fine because 5 is a concrete number literal.
leaked : Data
leaked = leak (mkData 5 11) -- Remember, remember...

_ : leaked ≡ mkData 5 5
_ = refl