content: ---
  layout: post
  title: "Isomorphisms"
  date: 2016-24-12 
  author: Vikraman Choudhury 
  published: false
  comments: true
  external-url:
  categories: basic
  demo: Iso.hs
  ---
  
  \begin{comment}
  \begin{code}
  {-@ LIQUID "--higherorder" @-}
  {-@ LIQUID "--totalhaskell" @-}
  {-@ LIQUID "--exactdc" @-}
  {-@ LIQUID "--diffcheck" @-}
  
  module Iso where
  
  import Language.Haskell.Liquid.ProofCombinators
  \end{code}
  \end{comment}
  
  In this blog post, we show how to use Liquid Haskell to build "verified" typeclasses. A verified typeclass allows one to
  express typeclass laws directly as Haskell code. We also show a technique to build verified instances and scale them up
  to compound datatypes using isomorphisms.
  
  First, we'll express verified typeclasses using Haskell records, but with LiquidHaskell refinements to express laws. As
  an example, let's define `VerifiedOrd`, which is the same as the `Ord` typeclass, but with total order laws added.
  
  \begin{code}
  {-@ data VerifiedOrd a = VerifiedOrd {
        leq     :: a -> a -> Bool
      , refl    :: x:a -> { Prop (leq x x) }
      , antisym :: x:a -> y:a -> { Prop (leq x y) && Prop (leq y x) ==> x == y }
      , trans   :: x:a -> y:a -> z:a -> { Prop (leq x y) && Prop (leq y z) ==> Prop (leq x z) }
      , total   :: x:a -> y:a -> { Prop (leq x y) || Prop (leq y x) }
      }
  @-}
  data VerifiedOrd a = VerifiedOrd {
      leq     :: a -> a -> Bool
    , refl    :: a -> Proof
    , antisym :: a -> a -> Proof
    , trans   :: a -> a -> a -> Proof
    , total   :: a -> a -> Proof
  }
  \end{code}
  
  The `leq` function represents the `<=` operator in `Ord`, and `refl`, `antisym`, `trans`, `total`, express the
  reflexivity, antisymmetry, transitivity and totality properties respectively, that a total order requires. Notice how
  the refinements express the laws, and the actual code is simply a function that returns `Proof` or `()`.
  
  Now, let's see how to define some simple verified instances. We need to instantiate `leq` for our type, "reflect" it
  into the logic, and prove all the required properties. For primitive types like `Int` or `Double`, it's "trivial"
  because we trust the SMT solver which already knows about integers.
  
  \begin{code}
  {-@ axiomatize leqInt @-}
  leqInt :: Int -> Int -> Bool
  leqInt x y = x <= y
  
  {-@ leqIntRefl :: x:Int -> { leqInt x x } @-}
  leqIntRefl :: Int -> Proof
  leqIntRefl x = leqInt x x ==. x <= x *** QED
  
  {-@ leqIntAntisym :: x:Int -> y:Int -> { leqInt x y && leqInt y x ==> x == y } @-}
  leqIntAntisym :: Int -> Int -> Proof
  leqIntAntisym x y = (leqInt x y && leqInt y x) ==. (x <= y && y <= x) ==. x == y *** QED
  
  {-@ leqIntTrans :: x:Int -> y:Int -> z:Int -> { leqInt x y && leqInt y z ==> leqInt x z } @-}
  leqIntTrans :: Int -> Int -> Int -> Proof
  leqIntTrans x y z = (leqInt x y && leqInt y z) ==. (x <= y && y <= z) ==. x <= z ==. leqInt x z *** QED
  
  {-@ leqIntTotal :: x:Int -> y:Int -> { leqInt x y || leqInt y x } @-}
  leqIntTotal :: Int -> Int -> Proof
  leqIntTotal x y = (leqInt x y || leqInt y x) ==. (x <= y || y <= x) *** QED
  
  vordInt :: VerifiedOrd Int
  vordInt = VerifiedOrd leqInt leqIntRefl leqIntAntisym leqIntTrans leqIntTotal
  \end{code}
  
  How about a complex datatype? Let's consider an inductive datatype, the peano natural numbers. Not surprisingly, the
  proofs follow by induction. For conciseness, we only show totality and elide the rest.
  
  \begin{code}
  {-@ data Peano [toNat] = Z | S Peano @-}
  data Peano = Z | S Peano deriving (Eq)
  
  {-@ measure toNat @-}
  {-@ toNat :: Peano -> { n:Int | 0 <= n } @-}
  toNat :: Peano -> Int
  toNat Z = 0
  toNat (S n) = 1 + toNat n
  
  {-@ axiomatize leqPeano @-}
  leqPeano :: Peano -> Peano -> Bool
  leqPeano Z _ = True
  leqPeano _ Z = False
  leqPeano (S n) (S m) = leqPeano n m
  
  {-@ leqNTotal :: n:Peano -> m:Peano -> {(leqPeano n m) || (leqPeano m n)} / [toNat n + toNat m] @-}
  leqNTotal :: Peano -> Peano -> Proof
  leqNTotal Z m = leqPeano Z m *** QED
  leqNTotal n Z = leqPeano Z n *** QED
  leqNTotal (S n) (S m)
    =   (leqPeano (S n) (S m) || leqPeano (S m) (S n))
    ==. (leqPeano n m || leqPeano (S m) (S n)) ? (leqNTotal n m )
    ==. (leqPeano n m || leqPeano m n) ? (leqNTotal m n)
    *** QED
  \end{code}
  
  Writing down proofs for more complex datatypes is tedious, it requires case analysis for each constructor and using the
  induction hypothesis. However, we can decompose Haskell datatypes into sums and products, and we can build up compound
  proofs using isomorphisms! To that end, we design some machinery to express isomorphisms, and prove that laws are
  preserved under isomorphic images.
  
  \begin{code}
  {-@ data Iso a b = Iso {
        to   :: a -> b
      , from :: b -> a
      , tof  :: y:b -> { to (from y) == y }
      , fot  :: x:a -> { from (to x) == x }
      }
  @-}
  data Iso a b = Iso {
      to   :: a -> b
    , from :: b -> a
    , tof  :: b -> Proof
    , fot  :: a -> Proof
  }
  \end{code}
  
  An isomorphism between types `a` and `b` is a pair of functions `to :: a -> b` and `from :: b -> a` that are mutually
  inverse to each other. We now claim that total order laws are preserved under `Iso`; this amounts to building up a
  `VerifiedOrd b`, given a `VerifiedOrd a` and an `Iso a b`.
  
  \begin{code}
  {-@ axiomatize leqFrom @-}
  leqFrom :: (a -> a -> Bool)
          -> (b -> a)
          -> (b -> b -> Bool)
  leqFrom leqa from x y = leqa (from x) (from y)
  
  {-@ leqFromRefl :: leqa:(a -> a -> Bool) -> leqaRefl:(x:a -> { Prop (leqa x x) })
                  -> from:(b -> a)
                  -> x:b -> { leqFrom leqa from x x }
  @-}
  leqFromRefl :: (a -> a -> Bool) -> (a -> Proof)
              -> (b -> a)
              -> b -> Proof
  leqFromRefl leqa leqaRefl from x =
        leqFrom leqa from x x
    ==. leqa (from x) (from x)
    ==. True ? leqaRefl (from x)
    *** QED
  
  {-@ leqFromAntisym :: leqa:(a -> a -> Bool)
                     -> leqaAntisym:(x:a -> y:a -> { Prop (leqa x y) && Prop (leqa y x) ==> x == y })
                     -> to:(a -> b) -> from:(b -> a) -> tof:(y:b -> { to (from y) == y })
                     -> x:b -> y:b -> { leqFrom leqa from x y && leqFrom leqa from y x ==> x == y }
  @-}
  leqFromAntisym :: (Eq a, Eq b)
                 => (a -> a -> Bool) -> (a -> a -> Proof)
                 -> (a -> b) -> (b -> a) -> (b -> Proof)
                 -> b -> b -> Proof
  leqFromAntisym leqa leqaAntisym to from tof x y
    =   (leqFrom leqa from x y && leqFrom leqa from y x)
    ==. (leqa (from x) (from y) && leqa (from y) (from x))
    ==. from x == from y ? leqaAntisym (from x) (from y)
    ==. to (from x) == to (from y)
    ==. x == to (from y) ? tof x
    ==. x == y           ? tof y
    *** QED
  
  {-@ leqFromTrans :: leqa:(a -> a -> Bool)
                   -> leqaTrans:(x:a -> y:a -> z:a -> { Prop (leqa x y) && Prop (leqa y z) ==> Prop (leqa x z) })
                   -> from:(b -> a)
                   -> x:b -> y:b -> z:b
                   -> { leqFrom leqa from x y && leqFrom leqa from y z ==> leqFrom leqa from x z }
  @-}
  leqFromTrans :: (a -> a -> Bool) -> (a -> a -> a -> Proof)
               -> (b -> a)
               -> b -> b -> b -> Proof
  leqFromTrans leqa leqaTrans from x y z =
        (leqFrom leqa from x y && leqFrom leqa from y z)
    ==. (leqa (from x) (from y) && leqa (from y) (from z))
    ==. leqa (from x) (from z) ? leqaTrans (from x) (from y) (from z)
    ==. leqFrom leqa from x z
    *** QED
  
  {-@ leqFromTotal :: leqa:(a -> a -> Bool) -> leqaTotal:(x:a -> y:a -> { Prop (leqa x y) || Prop (leqa y x) })
                   -> from:(b -> a) -> x:b -> y:b -> { leqFrom leqa from x y || leqFrom leqa from y x }
  @-}
  leqFromTotal :: (a -> a -> Bool) -> (a -> a -> Proof)
               -> (b -> a) -> b -> b -> Proof
  leqFromTotal leqa leqaTotal from x y =
        (leqFrom leqa from x y || leqFrom leqa from y x)
    ==. (leqa (from x) (from y) || leqa (from y) (from x))
    ==. True ? leqaTotal (from x) (from y)
    ==. leqFrom leqa from y x
    *** QED
  
  vordIso :: (Eq a, Eq b) => Iso a b -> VerifiedOrd a -> VerifiedOrd b
  vordIso (Iso to from tof fot) (VerifiedOrd leqa leqaRefl leqaAntisym leqaTrans leqaTotal) =
    VerifiedOrd
      (leqFrom leqa from)
      (leqFromRefl leqa leqaRefl from)
      (leqFromAntisym leqa leqaAntisym to from tof)
      (leqFromTrans leqa leqaTrans from)
      (leqFromTotal leqa leqaTotal from)
  \end{code}
  
  We can now write a `VerifiedOrd` for `Peano` by mapping it onto `type Nat = { n:Int | 0 <= n }`, which is easier to
  prove properties about because it's just an integer!
  
  \begin{code}
  {-@ type Nat = { n:Int | 0 <= n } @-}
  type Nat = Int
  
  {-@ axiomatize fromNat @-}
  {-@ fromNat :: Nat -> Peano @-}
  fromNat :: Nat -> Peano
  fromNat n
    | n == 0 = Z
    | otherwise = S (fromNat (n - 1))
  
  {-@ toFrom :: x:Nat -> { toNat (fromNat x) == x } @-}
  toFrom :: Nat -> Proof
  toFrom n
    | n == 0 = toNat (fromNat 0) ==. toNat Z ==. 0 *** QED
    | n > 0 = toNat (fromNat n)
          ==. toNat (S (fromNat (n - 1)))
          ==. 1 + toNat (fromNat (n - 1))
          ==. 1 + (n - 1) ? toFrom (n - 1)
          ==. n
          *** QED
  
  {-@ fromTo :: x:Peano -> { fromNat (toNat x) == x } @-}
  fromTo :: Peano -> Proof
  fromTo Z = fromNat (toNat Z) ==. fromNat 0 ==. Z *** QED
  fromTo (S n) = fromNat (toNat (S n))
             ==. fromNat (1 + toNat n)
             ==. S (fromNat ((1 + toNat n) - 1))
             ==. S (fromNat (toNat n))
             ==. S n ? fromTo n
             *** QED
  
  {-@ isoNatPeano :: Iso Nat Peano @-}
  isoNatPeano :: Iso Nat Peano
  isoNatPeano = Iso fromNat toNat fromTo toFrom
  
  vordNat :: VerifiedOrd Nat
  vordNat = VerifiedOrd leqInt leqIntRefl leqIntAntisym leqIntTrans leqIntTotal
  
  vordPeano :: VerifiedOrd Peano
  vordPeano = vordIso isoNatPeano vordNat
  \end{code}
  
  Similarly, we can break down compound datatypes into sums and products, just like what happens in `GHC.Generics`, and
  use the isomorphism to write down `VerifiedOrd` instances. We do however need to provide instances of `VerifiedOrd` for
  sums and products.
  
  \begin{code}
  vordProd :: VerifiedOrd a -> VerifiedOrd b -> VerifiedOrd (a, b)
  vordSum :: VerifiedOrd a -> VerifiedOrd b -> VerifiedOrd (Either a b)
  \end{code}
  
  \begin{comment}
  \begin{code}
  vordSum = undefined
  vordProd = undefined
  \end{code}
  \end{comment}
  
  Our [library](https://github.com/iu-parfunc/verified-instances) explores this idea to build some verified typeclasses,
  such as `VerifiedOrd` and `VerifiedMonoid`. We also provide combinators to build verified instances by using
  isomorphisms. Also, using a [reflection hack](https://www.schoolofhaskell.com/user/thoughtpolice/using-reflection), we
  can reify these "verified" terms to typeclass dictionaries at runtime, to call legacy functions which require `Ord`
  constraints and so on.
  