Full specification of HF ZIpper as given (doesn't actually work)

hf_full.idr

-- Example 3.8 from Hanmana and Fiore - page 63
-- (Foundations of GADTS and Inductive Families)

data Expr : Type -> Type where
  Const : Int -> Expr Int
  IsZero : Expr Int -> Expr Bool
  If : Expr Bool -> Expr a -> Expr a -> Expr a

-- Page 66: Context specialised for the Expr type above
--   General form for non-root cases is:
--   Name : ChildExprTy₁ -> ChildExpr2₂ ... -> ChildExprTyₙ ->
--          CurrentContextTy -> Ctx (ChildExprTyₕ)
data Ctx : Type -> Type where
  -- Unifies with any type (Called [] in HF paper).
  Root : Ctx a
  -- we don't need a constructor for Const, it's a non-branching leaf node.
  -- Is zero has no sibling expressions for its children so it just needs a context.
  IsZeroHole : Ctx Bool -> Ctx Int
  -- If has three holes (left, middle, down)
  IfLeftHole : Expr a -> Expr a -> Ctx a -> Ctx Bool
  IfMidHole : Expr Bool -> Expr a -> Ctx a -> Ctx a
  IfRightHole : Expr Bool -> Expr a -> Ctx a -> Ctx a

-- Page 66 : Zipper specialised for Expr type above.
data Zipper : Type -> Type where
  -- NB : My ▷ has to be prefix instead of infix like the paper shows.
   ▷ : Expr a -> Ctx a -> Zipper a
   Fail : Zipper a
  
-- We now define a pair of functions upₖ and downₖ where k is every
-- possible hole traversal combination.

downFromIsZero : Zipper Bool -> Zipper Int
-- first destruct on Zipper (▷ and Fail).
-- then destruct on the first argument to ▷ (The Expression).
-- We then construct the appropriate Context on the RHS and use the Expr in
-- scope.
downFromIsZero (▷ (IsZero x) ctx) = ▷ x (IsZeroHole ctx) -- our one valid case
downFromIsZero (▷ _ _) = Fail -- fail on all other cases
downFromIsZero Fail = Fail

upFromIsZero : Zipper Int -> Zipper Bool
-- when going up we first destruct the Zipper.
-- Then we destruct the second argument to ▷ (The Context).
-- We then construct the appropriate Expr on the RHS and use the Ctx
-- in scope.
upFromIsZero (▷ n (IsZeroHole ctx)) = ▷ (IsZero n) ctx
upFromIsZero (▷ _ _) = Fail -- fail on all other cases
upFromIsZero Fail = Fail

downFromIfLeft : Zipper a -> Zipper Bool
downFromIfLeft (▷ (If p t f) ctx) = ▷ p (IfLeftHole t f ctx)
downFromIfLeft (▷ _ _) = Fail
downFromIfLeft Fail = Fail


-- ************************ ANOTHER PROBLEM CASE ****************************
--
-- This also fails to typecheck for the same reasons as our function
-- example. A ≠ A₀. 
--
-- This does work if we wrap the return type in a Σ type.
--
-- In short it is not possible to specify the HF zipper in modern dependently
-- typed languages as given in their paper if the return type of any traversal
-- function requires moving from a known type to a polymorphic type.
upFromIfLeft : Zipper Bool -> Zipper a
upFromIfLeft (▷ p (IfLeftHole {a} t f ctx)) = ▷ (If p t f) ctx
upFromIfLeft (▷ _ _ ) = Fail
upFromIfLeft Fail = Fail

-- Going from some polymorphic a to the same a is fine.
downFromIfMid : Zipper a -> Zipper a
downFromIfMid (▷ (If p t f) ctx) = ▷ t (IfMidHole p f ctx)
downFromIfMid (▷ _ _) = Fail
downFromIfMid Fail = Fail

-- unfortunately I had to add the failing cases explitly here.
upFromIfMId : Zipper a -> Zipper a
upFromIfMId (▷ t Root) = Fail
upFromIfMId (▷ t (IsZeroHole _)) = Fail
upFromIfMId (▷ t (IfLeftHole _ _ _)) = Fail
upFromIfMId (▷ t (IfMidHole p f ctx)) = ▷ (If p t f) ctx
upFromIfMId (▷ t (IfRightHole x y z)) = Fail
upFromIfMId Fail = Fail

downFromIfRight : Zipper a -> Zipper a
downFromIfRight (▷ (If p t f) ctx) = ▷ f (IfRightHole p t ctx)
downFromIfRight (▷ _ _ ) = Fail
downFromIfRight Fail = Fail

upfromIfLeft : Zipper a -> Zipper a
upfromIfLeft (▷ f Root) = Fail
upfromIfLeft (▷ f (IsZeroHole x)) = Fail
upfromIfLeft (▷ f (IfLeftHole x y z)) = Fail
upfromIfLeft (▷ f (IfMidHole x y z)) = Fail
upfromIfLeft (▷ f (IfRightHole p t ctx)) = ▷ (If p t f) ctx 
upfromIfLeft Fail = Fail

-- The plug functions given on page 65 are only discussed on a Nat indexed 
-- GADT. The actual substitution functions are more complex over Type index
-- GADTs but we don't really want to substitute inside our Expr type 
-- (we can construct using Const easily enough!) we just want to update our zipper type.
plug : Expr a -> Zipper a -> Zipper a
plug x (▷ y ctx) = ▷ x ctx
plug x Fail = Fail


exampleExpr : Expr Int
exampleExpr = If (IsZero (Const 2)) (Const 3) (Const 0)

exampleZip : Zipper Int
exampleZip = ▷ exampleExpr Root
-- ▷ (If (IsZero (Const 2)) (Const 3) (Const 0)) Root

moveToLowestLeftNode : Zipper Int
moveToLowestLeftNode = downFromIsZero (downFromIfLeft exampleZip)
-- ▷ (Const 2) (IsZeroHole (IfLeftHole (Const 3) (Const 0) Root))

updatedFocus : Zipper Int
updatedFocus = plug (Const 0) moveToLowestLeftNode

moveUpFromLowestLeftNode : Zipper Int
moveUpFromLowestLeftNode = upFromIfLeft (upFromIsZero updatedFocus)
-- ▷ (If (IsZero (Const 0)) (Const 3) (Const 0)) Root