compact usage of Except

Stream: new members

[JJ]

I have converted some code previously using Option α to Except ε α. Due to losing the auto-conversion of α -> Option α, and the compactness of none vs. Except.error err, the code is quite a bit more verbose. Does anyone have advice for golfing this down?

import Lean.Data.AssocList

-- We implement a useful helper method on Option for conversion to Except.
namespace Option
  def toExcept (self : Option α) (err : ε) : Except ε α :=
    match self with
    | .some a => Except.ok a
    | .none => Except.error err
end Option

-- We consider types separate from terms, to start.
-- TODO: how to rename identifiers locally? would like to use Type
inductive Type' where
| Nat
| Func (a b : Type')
deriving BEq  -- structural equality is enough, for now.

-- The simply typed lambda calculus.
inductive Expr where
-- Nat
| zero
| succ (num : Expr)
| ind (num base step : Expr) (type : Type')
-- Func
| abs (name : String) (body : Expr)
| app (func arg : Expr)
| var (name : String)
-- Type'
| the (expr : Expr) (type : Type')

instance : ToString Type' := ⟨toString⟩
where toString : Type' -> String
| .Nat => "Nat" | .Func a b => s!"{toString a} → {toString b}"

instance : ToString Expr := ⟨toString⟩
where toString : Expr -> String
| .zero => s!"0"
| .succ num => s!"{toString num} ++"
| .ind num base step type => s!"(ind {type} {toString num} {toString base} {toString step})"
| .abs name body => s!"(λ.{name} {toString body})"
| .app func arg => s!"{toString func} {toString arg}"
| .var name => name
| .the expr type => s!"({toString expr} : {type})"

-- The type context is a mapping from names to types.
abbrev Context := Lean.AssocList String Type'

-- Check an expression against a given type.
partial def check (expr : Expr) (type : Type') (ctx : Context) : Bool :=
  match expr with
  | .zero => type == .Nat
  | .succ num => type == .Nat && check num .Nat ctx
  | .abs name body =>
    match type with
    | .Func a b => check body b (ctx.cons name a)
    | .Nat => false
  | _ =>
    match synth expr ctx with
    | .ok type' => type == type'
    | .error _ => false

-- Synthesize a type from an expression, if possible.
-- We report useful error messages on failure.
-- TODO: with ε ≠ α, any nice way to automagically convert types?
where synth (expr : Expr) (ctx : Context) : Except String Type' := do
  match expr with
  | .zero => Except.ok Type'.Nat
  | .succ num =>
    if check num .Nat ctx then Except.ok Type'.Nat
    else Except.error s!"expression {num} not of type Nat at {expr}"
  | .the expr type =>
    if check expr type ctx then Except.ok type
    else Except.error s!"expression {expr} not of type {type}"
  | .ind num base step type =>
    let num_type <- synth num ctx
    if num_type == .Nat then
      if check base type ctx then
        if check step (.Func .Nat (.Func type type)) ctx then
          Except.ok type
        else Except.error "step {step} of incorrect type"
      else Except.error "base {base} of incorrect type"
    else Except.error "num {num} not of type Nat"
  | .app func arg =>
    let func_type <- synth func ctx
    match func_type with
    | .Func a b =>
      if check arg a ctx then Except.ok b
      else Except.error s!"argument {arg} not of type {a} at {expr}"
    | .Nat => Except.error "attempting to apply an argument to a Nat"
  | .var name => ctx.find? name |>.toExcept "name {name} not found in context"
  | .abs _ _ => Except.error "cannot synth polymorphic type of abstraction name at {expr}"

[JJ]

I would still be interested in any advice here :-)

[JJ]

Hmm, an open Except helped quite a bit. I think it might be neat to auto convert non-string types to Except.ok, but obvs seem why this would be bad, too... prefixing everything with ok <| isn't half bad.

[Kyle Miller]

There's dotted function notation as an alternative to open Except. I see you're already using it with .Func, etc. You can write .ok and .error.

However, given that you are using do notation, any reason you're not using return and throw?

[JJ]

I was unaware throw existed!

[Kyle Miller]

There's also making use of do more and making a function to help you check conditions.

where synth (expr : Expr) (ctx : Context) : Except String Type' := do
  let guardOrThrow (b : Bool) (msg : Unit → String) : Except String Unit := do
    unless b do throw (msg ())
  match expr with
  | .zero => return Type'.Nat
  | .succ num =>
    guardOrThrow (check num .Nat ctx) fun _ => s!"expression {num} not of type Nat at {expr}"
    return Type'.Nat
  | .the expr type =>
    guardOrThrow (check expr type ctx) fun _ => s!"expression {expr} not of type {type}"
    return type
  | .ind num base step type =>
    let num_type <- synth num ctx
    guardOrThrow (num_type == .Nat) fun _ => s!"num {num} not of type Nat"
    guardOrThrow (check base type ctx) fun _ => s!"base {base} of incorrect type"
    guardOrThrow (check step (.Func .Nat (.Func type type)) ctx) fun _ => s!"step {step} of incorrect type"
    return type
  | .app func arg =>
    let func_type <- synth func ctx
    match func_type with
    | .Func a b =>
      guardOrThrow (check arg a ctx) fun _ => s!"argument {arg} not of type {a} at {expr}"
      return b
    | .Nat => throw "attempting to apply an argument to a Nat"
  | .var name => ctx.find? name |>.toExcept s!"name {name} not found in context"
  | .abs _ _ => throw s!"cannot synth polymorphic type of abstraction name at {expr}"

The Unit -> String is to make sure you avoid creating the string unless the error occurs.

[Eric Wieser]

guardOrThrow (c) fun _ => msg

is longer than what it replaces!

unless c do throw msg