Type Systems, One Tool: The Cells the Four Do Not Occupy

The parent note implements one reversible-transform tool in TypeScript, Rust, Dafny, and Racket. All four write encode and decode as separate functions and then reconcile them: TypeScript reports the mismatch at runtime, Rust makes decode an Option, Dafny proves decode(encode(x))==x, Racket blames whoever breaks it at the boundary.

None of them derives the inverse. The round-trip law is always a checked relation between two independently authored artifacts.

The axis the four never touch: invertibility by construction, where the codec is one artifact and both directions fall out of it, so the round-trip law holds structurally rather than being verified.

The Haskell lens library (Kmett 2012) provides Iso, the optic for isomorphisms. An Iso' s a gives you view (forward) and review (backward) from a single definition. The round-trip law review . view = id is structural, not checked.

-- Verified: GHC 9.10.3, lens 5.3.6, FreeBSD 15.0
import Control.Lens

-- ROT13 as an Iso: one artifact, both directions fall out.
-- The involution case: encode IS decode, so the Iso is its own inverse.
rot13 :: Iso' String String
rot13 = iso encode encode
  where
    encode = map rot
    rot c
      | c >= 'a' && c <= 'z' = toEnum $ (fromEnum c - fromEnum 'a' + 13) `mod` 26 + fromEnum 'a'
      | c >= 'A' && c <= 'Z' = toEnum $ (fromEnum c - fromEnum 'A' + 13) `mod` 26 + fromEnum 'A'
      | otherwise = c

ghci> view rot13 "Hello World"
"Uryyb Jbeyq"
ghci> review rot13 "Uryyb Jbeyq"
"Hello World"
ghci> review rot13 (view rot13 "Hello World") == "Hello World"
True

The key test is composition through the optics lattice. Compose two Iso values and you get an Iso. The type checker tracks this:

-- Iso . Iso = Iso (both directions survive composition)
rot26 :: Iso' String String
rot26 = rot13 . rot13  -- composes to identity

-- Caesar(n) as a non-self-inverse bijection
caesar :: Int -> Iso' String String
caesar n = iso (shift n) (shift (-n))
  where
    shift k = map $ \c ->
      if c >= 'a' && c <= 'z'
        then toEnum $ (fromEnum c - fromEnum 'a' + k) `mod` 26 + fromEnum 'a'
        else c

ghci> view rot26 "Test"
"Test"
ghci> view (caesar 3) "abc"
"def"
ghci> review (caesar 3) "def"
"abc"
ghci> review (caesar 3) (view (caesar 3) "hello") == "hello"
True

The four-way taxonomy in the parent note (Involution / Bijection / Parameterized / Surjection) is not a fresh sum type. It is the profunctor-optics subtyping lattice (Pickering, Gibbons, and Wu 2017) with the names changed:

-- The mapping:
-- Involution    ~ Iso that is its own inverse  (re . re = id)
-- Bijection     ~ Iso                          (review . view = id)
-- Parameterized ~ args -> Iso s a              (factory producing an optic)
-- Surjection    ~ Getter / Fold                (has view, has NO review)

The thing the optics encoding reads off that enum CodecPattern cannot: the subtyping is real. An Iso weakens to a Getter, so "drop reversibility" is an upcast the type checker tracks, and "recover it" is a downcast you cannot write.

import Control.Lens

-- A surjection: toUpper has view but no review.
-- It is a Getter, not an Iso. The type system forbids `review`.
upperGetter :: Getter String String
upperGetter = to (map toUpper)
  where toUpper c | c >= 'a' && c <= 'z' = toEnum (fromEnum c - 32)
                  | otherwise = c

ghci> view upperGetter "Hello"
"HELLO"
ghci> review upperGetter "HELLO"
<interactive>: error:
    Couldn't match type 'Const String String'
                   with 'Identity String'
    -- The type system refuses: a Getter has no review.

Compose anything with a Getter and you get a Getter:

ghci> :t rot13 . upperGetter
-- Error: Getter does not compose on the right of an Iso in review position
-- The lattice join computes automatically.

This is the chain-reversibility property (the runtime isReversible fold in the parent note) lifted to the type level. None of the four implementations do this. Rust's Option<CodecFn> encodes the presence of an inverse as a value; profunctor optics encode it as the position in a lattice, and composition computes the join automatically.

Boomerang (Foster et al. 2007) implements bidirectional string transformations where the parser and printer are derived from a single description. The well-behavedness laws (GetPut, PutGet) are exactly the round-trip laws from the codec spec, stated as the lens type itself.

-- Verified: boomerang 1.4.9.4, GHC 9.10.3
import Text.Boomerang.String
import Text.Boomerang.Combinators

The prior art is already in the parent note's bibliography by author: Foster-Greenwald-Moore-Pierce-Schmitt, "Combinators for Bidirectional Tree Transformations" (TOPLAS 2007). Pierce is the same Pierce as Types and Programming Languages (Pierce 2002).

Refutation for including the lens cell: if the codec set is dominated by surjections and parameterized factories, lenses buy little. A one-string-to-one-string bijection is a degenerate Iso, and the lens machinery (get/put/create) is overkill for codecs that are not view-update. The cell earns its place only if involutions and bijections dominate the registry.

Rust encodes "this can fail / has no inverse" structurally as Result and Option. Koka (Leijen 2017) puts the same fact on a different axis: a row of effects. A surjection's decode is not an absent value but a function carrying <exn> or simply not typeable as total; the codec's signature reads string -> <div|exn> string. This is a cleaner separation because purity and totality are the default and failure is annotated, rather than failure being a return-type wrapper you thread by hand.

For the "what does the type carry" column it adds a fifth answer: the effect carries the partiality, orthogonal to affine ownership.

The parent note cites Jhala-Vazou (Jhala and Vazou 2021) but implements refinement only in Dafny. Two cells are missing:

• Liquid Haskell (Vazou et al., Haskell Symposium 2014) – the literal vehicle of the tutorial cited. Same decode(encode(x))==x as a refinement, but inside the optics/typeclass ecosystem, so you can state the law and the lattice in one language. Sits between Rust and Dafny on one toolchain.
• F* (Swamy et al., POPL 2016) – refinement + effects + extraction to OCaml/F#. The fact Dafny under-sells: the verified artifact and the running artifact are the same program.

Stainless/Scala is the mainstream-language version of the same point for the cost argument in the parent note's section on when not to.

In all four implementations, the reversibility of the whole pipeline (isReversible, firstIrreversibleStep) is computed at runtime – a fold over per-step results. It is the one invariant the type systems never state statically.

Whether that is a gap depends on a fact in the spec: if chain-reversibility is just "all steps reversible implies chain reversible" (a fold of conjunction), it is a trivial type-level fold, not a verification problem. But the Dafny port's [SG-n] markers flag cross-step domain preconditions (base64:d requires valid base64). Those preconditions make composition non-commutative and order-sensitive: codec B is reversible only on the output domain of codec A. That is a relational closure question, and it earns:

• Alloy (Jackson, Software Abstractions) – the codec registry as relations, "which chains round-trip" as a relational-closure check over the precondition graph. Finds the counterexample chain the per-codec types cannot see.
• TLA+ – the pipeline-as-sequential-composition with domain guards is a reachability property (firstIrreversibleStep is the first state violating the round-trip invariant), which is a model-checking statement, not a per-codec one.

The TypeScript section (structural, erasable) and the Racket section (contracts

• blame) are the two endpoints of gradual typing, and the parent note never

names the theory connecting them. Typed Racket and the gradual guarantee (Siek-Taha 2006; Siek-Vitek-Tobin-Hochstadt-Garcia, SNAPL 2015) are the principled account of why Racket's boundary contracts are where blame lands when typed and untyped codecs interoperate. Not a new implementation cell, but the missing citation that makes TypeScript-to-Racket a continuum rather than two unrelated points.

The complete test program, tangled and executed on FreeBSD 15.0 with GHC 9.10.3 and lens 5.3.6.

-- file: test-axes.hs
-- Tangle and run: runghc test-axes.hs
-- Verified: GHC 9.10.3, lens 5.3.6, FreeBSD 15.0
{-# LANGUAGE RankNTypes #-}
import Control.Lens
import Data.Char (isLower, isUpper)

-- 1. Involution as Iso (self-inverse: encode IS decode)
rot13 :: Iso' String String
rot13 = iso enc enc
  where
    enc = map rot
    rot c
      | c >= 'a' && c <= 'z' = toEnum $ (fromEnum c - fromEnum 'a' + 13) `mod` 26 + fromEnum 'a'
      | c >= 'A' && c <= 'Z' = toEnum $ (fromEnum c - fromEnum 'A' + 13) `mod` 26 + fromEnum 'A'
      | otherwise = c

-- 2. Bijection as Iso (non-self-inverse)
caesar :: Int -> Iso' String String
caesar n = iso (shift n) (shift (-n))
  where
    shift k = map $ \c ->
      if isLower c then toEnum $ (fromEnum c - fromEnum 'a' + k) `mod` 26 + fromEnum 'a'
      else if isUpper c then toEnum $ (fromEnum c - fromEnum 'A' + k) `mod` 26 + fromEnum 'A'
      else c

-- 3. Surjection as Getter (no review -- the type forbids it)
upperGetter :: Getter String String
upperGetter = to (map toUpper')
  where toUpper' c | c >= 'a' && c <= 'z' = toEnum (fromEnum c - 32)
                   | otherwise = c

-- Test harness
check :: String -> Bool -> IO ()
check label ok = putStrLn $ (if ok then "PASS" else "FAIL") ++ "  " ++ label

main :: IO ()
main = do
  putStrLn "=== Type Systems Axes: Literate Verification ==="
  putStrLn ""
  let hw = "Hello World"

  check "rot13 round-trip" $
    review rot13 (view rot13 hw) == hw

  check "rot13 self-inverse" $
    view rot13 (view rot13 hw) == hw

  check "caesar(3) round-trip" $
    review (caesar 3) (view (caesar 3) "hello") == "hello"

  check "caesar(3) not self-inverse" $
    view (caesar 3) (view (caesar 3) "hello") /= "hello"

  check "rot13 . rot13 = id" $
    view (rot13 . rot13) "Test" == "Test"

  check "upperGetter has view" $
    view upperGetter "hello" == "HELLO"

  check "caesar(3) . caesar(5) = caesar(8) round-trips" $
    review (caesar 8) (view (caesar 8) "abc") == "abc"

  check "all 25 caesar shifts round-trip" $
    all (\n -> review (caesar n) (view (caesar n) "test") == "test") [1..25]

  putStrLn ""
  putStrLn "=== Done ==="

• Type Systems for Software Developers: One Tool, Four Ways – the parent note
• Reversible Pipeline Transforms – the spec all implementations share