------------------------------------------------------------------------ -- The Agda standard library -- -- Zero-cost coercion to cross the FFI boundary ------------------------------------------------------------------------ {-# OPTIONS --cubical-compatible #-} module Foreign.Haskell.Coerce where ------------------------------------------------------------------------ -- Motivation -- Problem: No COMPILE directives for common inductive types -- In order to guarantee that the vast majority of the libary is -- considered safe by Agda, we had to remove the COMPILE pragmas -- associated to common inductive types. -- These directives cannot possibly be checked by the compiler and -- the user could define unsound mappings (e.g. swapping Bool's -- true and false). -- Solution: Essentially identical definitions + zero-cost coercions -- To solve this problem, we have introduced a number of essentially -- identical definitions in the Foreign.Haskell.* modules. However -- converting back and forth between the FFI-friendly type and its -- safe counterpart would take linear time. -- This module defines zero cost coercions between these types. ------------------------------------------------------------------------ -- Definition open import Level using (Level; _⊔_) open import Agda.Builtin.Nat open import Agda.Builtin.Int import IO.Primitive as STD import Data.List.Base as STD import Data.List.NonEmpty.Base as STD import Data.Maybe.Base as STD import Data.Product as STD import Data.Sum.Base as STD import Foreign.Haskell.Pair as FFI import Foreign.Haskell.Either as FFI import Foreign.Haskell.List.NonEmpty as FFI private variable a b c d e f : Level A : Set a B : Set b C : Set c D : Set d -- We define a simple indexed datatype `Coercible`. A value of `Coercible A B` -- is a proof that ̀A` and `B` have the same underlying runtime representation. -- The only possible proof is an incantation from the implementer begging to -- be trusted. -- We need this type to be concrete so that overlapping instances can be checked -- for equality: we do not care what proof we get as long as we get one. -- We need for it to be a data type rather than a record type so that Agda does -- not mistakenly build arbitrary instances by η-expansion. data Coercible (A : Set a) (B : Set b) : Set where TrustMe : Coercible A B {-# FOREIGN GHC data AgdaCoercible l1 l2 a b = TrustMe #-} {-# COMPILE GHC Coercible = data AgdaCoercible (TrustMe) #-} -- Once we get our hands on a proof that `Coercible A B` we postulate that it -- is safe to convert an `A` into a `B`. This is done under the hood by using -- `unsafeCoerce`. postulate coerce : {{_ : Coercible A B}} → A → B {-# FOREIGN GHC import Unsafe.Coerce #-} {-# COMPILE GHC coerce = \ _ _ _ _ _ -> unsafeCoerce #-} ------------------------------------------------------------------------ -- Unary and binary variants for covariant type constructors Coercible₁ : ∀ a c → (T : Set a → Set b) (U : Set c → Set d) → Set _ Coercible₁ _ _ T U = ∀ {A B} → {{_ : Coercible A B}} → Coercible (T A) (U B) Coercible₂ : ∀ a b d e → (T : Set a → Set b → Set c) (U : Set d → Set e → Set f) → Set _ Coercible₂ _ _ _ _ T U = ∀ {A B} → {{_ : Coercible A B}} → Coercible₁ _ _ (T A) (U B) ------------------------------------------------------------------------ -- Instances -- Nat -- Our first instance reveals one of Agda's secrets: natural numbers are -- represented by (arbitrary precision) integers at runtime! Note that we -- may only coerce in one direction: arbitrary integers may actually be -- negative and will not do as mere natural numbers. instance nat-toInt : Coercible Nat Int nat-toInt = TrustMe -- We then proceed to state that data types from the standard library -- can be converted to their FFI equivalents which are bound to actual -- Haskell types. -- Product pair-toFFI : Coercible₂ a b c d STD._×_ FFI.Pair pair-toFFI = TrustMe pair-fromFFI : Coercible₂ a b c d FFI.Pair STD._×_ pair-fromFFI = TrustMe -- Sum either-toFFI : Coercible₂ a b c d STD._⊎_ FFI.Either either-toFFI = TrustMe either-fromFFI : Coercible₂ a b c d FFI.Either STD._⊎_ either-fromFFI = TrustMe -- NonEmpty nonEmpty-toFFI : Coercible₁ a b STD.List⁺ FFI.NonEmpty nonEmpty-toFFI = TrustMe nonEmpty-fromFFI : Coercible₁ a b FFI.NonEmpty STD.List⁺ nonEmpty-fromFFI = TrustMe -- We follow up with purely structural rules for builtin data types which -- already have known low-level representations. -- Maybe coerce-maybe : Coercible₁ a b STD.Maybe STD.Maybe coerce-maybe = TrustMe -- List coerce-list : Coercible₁ a b STD.List STD.List coerce-list = TrustMe -- IO coerce-IO : Coercible₁ a b STD.IO STD.IO coerce-IO = TrustMe -- Function -- Note that functions are contravariant in their domain. coerce-fun : {{_ : Coercible A B}} → Coercible₁ c d (λ C → B → C) (λ D → A → D) coerce-fun = TrustMe -- Finally we add a reflexivity proof to discharge all the dangling constraints -- involving type variables and concrete builtin types such as `Bool`. -- This rule overlaps with the purely structural ones: when attempting to prove -- `Coercible (List A) (List A)`, should Agda use the proof obtained by `coerce-refl` -- or the one obtained by `coerce-list coerce-refl`? Because we are using a -- datatype with a single constructor these distinctions do not matter: both proofs -- are definitionally equal. coerce-refl : Coercible A A coerce-refl = TrustMe