Lea(r)n you a scheme

Stream: general

[Chris B]

I was flipping through this thing where you implement a version of scheme in Haskell. I'm curious whether there are any clever ways of implementing the given definition of the LispVal type in Lean. Trying to power through it as a mutual inductive (with a ListLispVal type to avoid nesting and making IFunc, and Eval part of the mutual) is no good since you end up with a negative occurrence in the Fun constructor.

In Haskell the whole thing is :

data LispVal =
    Atom T.Text
  | List [LispVal]
  | Number Integer
  | String T.Text
  | Fun IFunc
  | Lambda IFunc EnvCtx
  | Nil
  | Bool Bool

data IFunc = IFunc { fn :: [LispVal] -> Eval LispVal }
type EnvCtx = Map.Map T.Text LispVal
newtype Eval a = Eval { unEval :: ReaderT EnvCtx IO a }

In sort of pseudo-lean :

inductive LispVal
| Atom : string -> LispVal
| List : list LispVal -> LispVal
| Number : ℤ → LispVal
| String : string → LispVal
| Fun : IFunc → LispVal
| Lambda : IFunc → EnvCtx → LispVal
| Nil : LispVal
| Bool : bool → LispVal

structure IFunc :=
(fn : list LispVal → Eval LispVal)

def EnvCtx := KVMap string LispVal

structure Eval (A : Type) :=
(un_eval : reader_t EnvCtx io A)

[Mario Carneiro]

You can't represent these functions as functions in lean, because of nontermination

[Mario Carneiro]

If you are okay with meta you can do it, and if you are okay with adding termination conditions then I think you can do it as well

[Chris B]

You would still have to make some significant change to the type definition or break it up though right, since meta doesn't lift the ban on negative occurrences?
For termination condition do you just mean like gas?

[Mario Carneiro]

meta does lift the ban on negative occurrences

meta inductive term
| app : term → term → term
| lam : (term → term) → term

[Mario Carneiro]

import system.io

meta def EnvCtx := native.rb_map string
meta structure IFunc (A : Type) :=
(fn : list A → reader_t (EnvCtx A) io A)

meta inductive LispVal : Type
| Atom : string → LispVal
| List : list LispVal → LispVal
| Number : ℤ → LispVal
| String : string → LispVal
| Fun : IFunc LispVal → LispVal
| Lambda : IFunc LispVal → EnvCtx LispVal → LispVal
| Nil : LispVal
| Bool : bool → LispVal

[Mario Carneiro]

@Sebastian Ullrich Can you still do things like this in lean 4?

[Mario Carneiro]

neither partial nor unsafe seems to cover this use case for meta

[Chris B]

I guess you have to say the m word to get it to break.

** invalid mutually inductive type, non-positive occurrence in introduction rule: term -> term

meta mutual inductive term, val
with term : Type
| app : term → term → term
| lam : (term → term) → term
with val : Type
| mk : val

[Chris B]

That's a better definition than what I was trying to do anyway. Is the accepted way to newtype something to make it a def and mark it as irreducible, or is there another convention?

[Mario Carneiro]

structure gives you the most "newtype"-like semantics

[Mario Carneiro]

def is more like a typedef

[Sebastian Ullrich]

@Mario Carneiro sure https://github.com/leanprover/lean4/blob/5b296cbb33ac156ab262f231acb4f6cccc432056/tests/lean/run/inliner_loop.lean#L1