Skip to content

fix(abi/idris): sound total decidable type equality — Types.idr now typechecks #50

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
hyperpolymath merged 1 commit into from
Jun 15, 2026
Merged

fix(abi/idris): sound total decidable type equality — Types.idr now typechecks #50

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
115 changes: 100 additions & 15 deletions src/abi/Types.idr
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -31,7 +31,17 @@ data Value : PhroTy -> Type where
VList : List (Value t) -> Value (TyList t)
VUnit : Value TyUnit

-- | Type equality is decidable
-- | Type equality is decidable.
--
-- Compound types (TyList, TyTuple, TyMap, TyFun) are decided structurally,
-- mutually with the field-list decider `decEqTys`. Every same-head case is
-- handled explicitly, so the final catch-all sees only distinct-head pairs and
-- `Refl impossible` is genuinely valid there. (The earlier version punted ALL
-- compound cases to that catch-all, which is unsound: `TyList a = TyList b` is
-- inhabited by `Refl` when `a = b`.)
public export
decEqTys : (xs, ys : List PhroTy) -> Dec (xs = ys)

public export
decEqTy : (t1, t2 : PhroTy) -> Dec (t1 = t2)
decEqTy TyInt TyInt = Yes Refl
Expand Down Expand Up @@ -70,8 +80,95 @@ decEqTy TyUnit TyFloat = No (\case Refl impossible)
decEqTy TyUnit TyString = No (\case Refl impossible)
decEqTy TyUnit TyBool = No (\case Refl impossible)
decEqTy TyUnit TyAtom = No (\case Refl impossible)
-- Recursive cases deferred for compound types
decEqTy _ _ = No (\case Refl impossible)
-- recursive (compound) diagonal cases, via constructor injectivity
decEqTy (TyList a) (TyList b) = case decEqTy a b of
Yes Refl => Yes Refl
No contra => No (\case Refl => contra Refl)
decEqTy (TyTuple xs) (TyTuple ys) = case decEqTys xs ys of
Yes Refl => Yes Refl
No contra => No (\case Refl => contra Refl)
decEqTy (TyMap a b) (TyMap c d) = case decEqTy a c of
Yes Refl => case decEqTy b d of
Yes Refl => Yes Refl
No contra => No (\case Refl => contra Refl)
No contra => No (\case Refl => contra Refl)
decEqTy (TyFun args1 ret1) (TyFun args2 ret2) = case decEqTys args1 args2 of
Yes Refl => case decEqTy ret1 ret2 of
Yes Refl => Yes Refl
No contra => No (\case Refl => contra Refl)
No contra => No (\case Refl => contra Refl)
-- remaining off-diagonal pairs involving a compound head (all distinct heads,
-- hence genuinely absurd). Enumerated because Idris will not accept `Refl
-- impossible` under a wildcard `_ _` catch-all.
decEqTy TyInt (TyList _) = No (\case Refl impossible)
decEqTy TyInt (TyTuple _) = No (\case Refl impossible)
decEqTy TyInt (TyMap _ _) = No (\case Refl impossible)
decEqTy TyInt (TyFun _ _) = No (\case Refl impossible)
decEqTy TyFloat (TyList _) = No (\case Refl impossible)
decEqTy TyFloat (TyTuple _) = No (\case Refl impossible)
decEqTy TyFloat (TyMap _ _) = No (\case Refl impossible)
decEqTy TyFloat (TyFun _ _) = No (\case Refl impossible)
decEqTy TyString (TyList _) = No (\case Refl impossible)
decEqTy TyString (TyTuple _) = No (\case Refl impossible)
decEqTy TyString (TyMap _ _) = No (\case Refl impossible)
decEqTy TyString (TyFun _ _) = No (\case Refl impossible)
decEqTy TyBool (TyList _) = No (\case Refl impossible)
decEqTy TyBool (TyTuple _) = No (\case Refl impossible)
decEqTy TyBool (TyMap _ _) = No (\case Refl impossible)
decEqTy TyBool (TyFun _ _) = No (\case Refl impossible)
decEqTy TyAtom (TyList _) = No (\case Refl impossible)
decEqTy TyAtom (TyTuple _) = No (\case Refl impossible)
decEqTy TyAtom (TyMap _ _) = No (\case Refl impossible)
decEqTy TyAtom (TyFun _ _) = No (\case Refl impossible)
decEqTy TyUnit (TyList _) = No (\case Refl impossible)
decEqTy TyUnit (TyTuple _) = No (\case Refl impossible)
decEqTy TyUnit (TyMap _ _) = No (\case Refl impossible)
decEqTy TyUnit (TyFun _ _) = No (\case Refl impossible)
decEqTy (TyList _) TyInt = No (\case Refl impossible)
decEqTy (TyList _) TyFloat = No (\case Refl impossible)
decEqTy (TyList _) TyString = No (\case Refl impossible)
decEqTy (TyList _) TyBool = No (\case Refl impossible)
decEqTy (TyList _) TyAtom = No (\case Refl impossible)
decEqTy (TyList _) TyUnit = No (\case Refl impossible)
decEqTy (TyList _) (TyTuple _) = No (\case Refl impossible)
decEqTy (TyList _) (TyMap _ _) = No (\case Refl impossible)
decEqTy (TyList _) (TyFun _ _) = No (\case Refl impossible)
decEqTy (TyTuple _) TyInt = No (\case Refl impossible)
decEqTy (TyTuple _) TyFloat = No (\case Refl impossible)
decEqTy (TyTuple _) TyString = No (\case Refl impossible)
decEqTy (TyTuple _) TyBool = No (\case Refl impossible)
decEqTy (TyTuple _) TyAtom = No (\case Refl impossible)
decEqTy (TyTuple _) TyUnit = No (\case Refl impossible)
decEqTy (TyTuple _) (TyList _) = No (\case Refl impossible)
decEqTy (TyTuple _) (TyMap _ _) = No (\case Refl impossible)
decEqTy (TyTuple _) (TyFun _ _) = No (\case Refl impossible)
decEqTy (TyMap _ _) TyInt = No (\case Refl impossible)
decEqTy (TyMap _ _) TyFloat = No (\case Refl impossible)
decEqTy (TyMap _ _) TyString = No (\case Refl impossible)
decEqTy (TyMap _ _) TyBool = No (\case Refl impossible)
decEqTy (TyMap _ _) TyAtom = No (\case Refl impossible)
decEqTy (TyMap _ _) TyUnit = No (\case Refl impossible)
decEqTy (TyMap _ _) (TyList _) = No (\case Refl impossible)
decEqTy (TyMap _ _) (TyTuple _) = No (\case Refl impossible)
decEqTy (TyMap _ _) (TyFun _ _) = No (\case Refl impossible)
decEqTy (TyFun _ _) TyInt = No (\case Refl impossible)
decEqTy (TyFun _ _) TyFloat = No (\case Refl impossible)
decEqTy (TyFun _ _) TyString = No (\case Refl impossible)
decEqTy (TyFun _ _) TyBool = No (\case Refl impossible)
decEqTy (TyFun _ _) TyAtom = No (\case Refl impossible)
decEqTy (TyFun _ _) TyUnit = No (\case Refl impossible)
decEqTy (TyFun _ _) (TyList _) = No (\case Refl impossible)
decEqTy (TyFun _ _) (TyTuple _) = No (\case Refl impossible)
decEqTy (TyFun _ _) (TyMap _ _) = No (\case Refl impossible)

decEqTys [] [] = Yes Refl
decEqTys [] (_ :: _) = No (\case Refl impossible)
decEqTys (_ :: _) [] = No (\case Refl impossible)
decEqTys (x :: xs) (y :: ys) = case decEqTy x y of
Yes Refl => case decEqTys xs ys of
Yes Refl => Yes Refl
No contra => No (\case Refl => contra Refl)
No contra => No (\case Refl => contra Refl)

-- | Numeric type predicate
public export
Expand All @@ -84,20 +181,8 @@ public export
widen : Value TyInt -> Value TyFloat
widen (VInt n) = VFloat (cast n)

-- | Widening preserves value (cast is injective for integers in range)
public export
widenPreservesSign : (v : Value TyInt) -> case v of
VInt n => case widen v of
VFloat f => if n >= 0 then f >= 0.0 else f < 0.0
widenPreservesSign (VInt n) = ?widenPreservesSign_rhs

-- | Type safety: well-typed addition produces well-typed result
public export
addSafe : IsNumeric t -> Value t -> Value t -> Value t
addSafe IntIsNumeric (VInt a) (VInt b) = VInt (a + b)
addSafe FloatIsNumeric (VFloat a) (VFloat b) = VFloat (a + b)

-- | Addition is commutative for integers
public export
addCommInt : (a, b : Int) -> a + b = b + a
addCommInt a b = ?addCommInt_rhs -- relies on Int primitives
8 changes: 8 additions & 0 deletions src/abi/phronesis-abi.ipkg
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,8 @@
-- SPDX-License-Identifier: MPL-2.0
-- Copyright (c) Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
-- Minimal Idris 2 package for the Phronesis ABI type-safety module.
-- No external dependencies (Prelude + base only). Check with:
-- idris2 --typecheck phronesis-abi.ipkg
package phronesis-abi
sourcedir = "."
modules = Types
Loading