Cleaner coercion

Stream: new members

[Garrison Venn]

In my solution to exercise 4.3.3.4.3. A Tracing Evaluator in the book Functional Programming in Lean.

I used an explicit manual coercion in the function

applyTraced

. This coercion transformed type GPrim Empty to GPrim (ToTrace (GPrim Empty)) with the following:

let nop : GPrim (ToTrace (GPrim Empty)) :=
        match op with
        | .plus => .plus
        | .minus => .minus
        | .times => .times

Beyond not fully understanding why the coercion would not be automatic, I was wonder if there was cleaner syntax for this.

Thanks in advance

Code:

inductive GExpr (op : Type) where
  | const : Int → GExpr op
  | prim : op → GExpr op → GExpr op → GExpr op

inductive GPrim (special : Type) where
  | plus
  | minus
  | times
  | other: special → GPrim special

def applyPrim [Monad m]
    (applySpecial : special → Int → Int → m Int) :
    GPrim special → Int → Int → m Int
  | GPrim.plus, x, y => pure (x + y)
  | GPrim.minus, x, y => pure (x - y)
  | GPrim.times, x, y => pure (x * y)
  | GPrim.other op, x, y => applySpecial op x y

def evaluateM [Monad m]
    (applySpecial : special → Int → Int → m Int) :
    GExpr (GPrim special) → m Int
  | GExpr.const i => pure I
  | GExpr.prim p e1 e2 =>
    evaluateM applySpecial e1 >>= fun v1 =>
    evaluateM applySpecial e2 >>= fun v2 =>
    applyPrim applySpecial p v1 v2

structure WithLog (logged : Type) (α : Type) where
  log : List logged
  val : α
deriving Repr

abbrev GLogged : Type := (GPrim Empty × Int × Int)

instance : Monad (WithLog GLogged) where
  pure x := ⟨[], x⟩
  bind
  | ⟨ll, val⟩, next =>
      match next val with
        -- order in order of appearance
      | ⟨nl, v⟩ => ⟨ll ++ nl, v⟩

inductive ToTrace (α : Type) : Type where
  | trace : α → ToTrace α

deriving instance Repr for Empty
deriving instance Repr for GPrim

abbrev GTrace : Type :=
  ToTrace (GPrim Empty) → Int → Int → WithLog GLogged Int

def emptyTraced : GTrace := fun _ _ _ => pure 0

def applyTraced : GTrace
   | .trace op, lhs, rhs =>
       -- Is there a way to use coercion for this
       let nop : GPrim (ToTrace (GPrim Empty)) :=
        match op with
        | .plus => .plus
        | .minus => .minus
        | .times => .times
       applyPrim (emptyTraced) nop lhs rhs >>= fun res =>
       ⟨[(op, lhs, rhs)], res⟩

[Eric Wieser]

I recommend defining

def GPrim.map {α β : Type} (f : α → β) : GPrim α → GPrim β
  | .plus => .plus
  | .minus => .minus
  | .times => .times
  | .other a => .other (f a)

[Eric Wieser]

Then nop is op.map nofun

[Garrison Venn]

Thanks!

Just to get used to Functors, I went with your example translated to:

instance : Functor GPrim where
  map f
  | .plus => .plus
  | .minus => .minus
  | .times => .times
  | .other a => .other (f a)

def applyTraced : GTrace
   | .trace op, lhs, rhs =>
       let nop : GPrim (ToTrace (GPrim Empty)) := nofun <$> op
       applyPrim (emptyTraced) nop lhs rhs >>= fun res =>
       ⟨[(op, lhs, rhs)], res⟩

However I don't really understand the use of nofun it this case. I view it like nomatch where it cannot be used. Though it is not being used in Functor.map above, in the applyTraced implementation, it is allowed to be "captured" in map's first argument. So that is throwing me off with my current lack luster intuition. Also it seems nofun can be "cast" to any single argument function type involving Empty (I guess). Any explanation or reference would be useful. I may not currently understand the given explanation, but I can save it for later perusal.
Thanks again

[Eric Wieser]

nofun is shorthand for fun x => nomatch x