Zulip Chat Archive

Stream: general

Topic: Lea(r)n you a scheme


view this post on Zulip Chris B (Mar 11 2020 at 18:59):

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)

view this post on Zulip Mario Carneiro (Mar 11 2020 at 19:18):

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

view this post on Zulip Mario Carneiro (Mar 11 2020 at 19:19):

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

view this post on Zulip Chris B (Mar 11 2020 at 19:36):

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?

view this post on Zulip Mario Carneiro (Mar 11 2020 at 20:18):

meta does lift the ban on negative occurrences

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

view this post on Zulip Mario Carneiro (Mar 11 2020 at 20:25):

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

view this post on Zulip Mario Carneiro (Mar 11 2020 at 20:31):

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

view this post on Zulip Mario Carneiro (Mar 11 2020 at 20:32):

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

view this post on Zulip Chris B (Mar 11 2020 at 20:59):

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

view this post on Zulip Chris B (Mar 11 2020 at 21:04):

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?

view this post on Zulip Mario Carneiro (Mar 11 2020 at 21:13):

structure gives you the most "newtype"-like semantics

view this post on Zulip Mario Carneiro (Mar 11 2020 at 21:13):

def is more like a typedef

view this post on Zulip Sebastian Ullrich (Mar 11 2020 at 21:40):

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


Last updated: May 12 2021 at 23:13 UTC