Using lean as a general language

Stream: new members

[misterdrgn]

Hi all. I've been reading about Lean4 with great interest, as the syntax largely looks like an improvement on Haskell. I'm interested in playing around with it as a general purpose programming language, rather than doing any math-specific applications. I know Lean is supposed to support general programming, but I see very little information about this (aside from the Functional Programming in Lean book, which is what piqued my curiosity). Is this something that people look at seriously? I recognize that the available libraries would be quite limited. I don't want to do anything crazy for now, probably just some command-line tools.

While I'm here, I'll ask a more specific question. Does Lean support existential types? In particular I'm interested in having a heterogeneous list, where I can look through the list and find all items of type _a_ for any given type. One way this is handled in other languages is with existential types (tied to, say, a type class), with support for upcasting to the existential type so you can put everything in a list, and then downcasting back to the original types when you extract items from the list. I'm also curious if this can be handled in Lean with an inductive type, but my initial attempt failed.

inductive Item where
| int (value: Int): Item
| float (value: Float): Item
| string (value: String): Item
deriving Repr

def getValue (valueType: α -> Item) (values: List Item): List α :=
  match values with
  | [] => []
  | (valueType x) :: xs => x :: getValue valueType xs
  | _ :: xs => getValue valueType xs

I was trying for something where I could call getValue Item.int mylist, but it doesn't work because valueType can't be used in a pattern match I guess.

Thanks for any help on these two admittedly quite separate questions, and I hope to become more involved with this community.

[Johan Commelin]

Re q1: Lean is mostly written in lean. So that is one example that serious programming can be done in Lean. Besides that, people have written several other tools, like a bibtex query tool, a ray tracer, etc...
But the ecosystem is indeed still in its early stages

[Tomas Skrivan]

The easiest way is to write three separate functions for every type, like this(untested as I'm on mobile):

def getInts : List Item -> List Into
| [] => []
l (.int n) :: l => n :: getInts l
| _ :: l => getInts l

To the first question on Lean as a programming language, it is definitely viable and there are a bunch of people using it that way however it is overshadowed by all the math related projects.

[misterdrgn]

@Johan Commelin Thanks. Honestly I’m less worried about the library support than I am about the lack of information online. If people here don’t mind being peppered with questions, then maybe it’s fine.

[misterdrgn]

@Tomas Skrivan Thank you, but I’m particularly interested in a general-purpose solution that won’t require additional code when new types are added. I’m mostly just curious about how Lean handles that kind of a problem.

[Tomas Skrivan]

Yeah, I am not a dependent type guru so there might be a way of having a general solution but I'm afraid that the naive function:

def getOfType (S : Type) : List ((T : Type) x T) -> List S := ...

Is impossible to implement. The only viable solution I can think of is:

inductive TypeTag
| int | float | string

def TypeTag.toType : TypeTag -> Type
| int => Int | float => Float | string => String

def getItems (s : TypeTag) : List ((t : TypeTag) x t.toType) -> List s.toType := ...

It is probably quite easy to write a macro that automatically generates these given a list of types. The crucial point is that you have to fix the set of types you want to work with.

[Johan Commelin]

@misterdrgn Please pepper this zulip with questions. If the end result is that people write more online docs/tutorials/etc... then that's a win (-;
I should note that there is very active work right now on writing a reference manual for Lean 4. So I'm confident that there will be high quality material for Lean core in the near future.

[Edward van de Meent]

there is the following pattern:

universe u

set_option autoImplicit false

class MyInterfaceSpec (T : Type u) where
  getType : T → String
  getString : (t:T) → (getType t = "String") → String
  -- whatever functions you need access to

structure MyInterface where
  {T : Type u}
  [toSpec : MyInterfaceSpec T]
  val : T


attribute [instance] MyInterface.toSpec

instance : MyInterfaceSpec (MyInterface) where
  getType x := MyInterfaceSpec.getType x.val
  getString x h := MyInterfaceSpec.getString x.val h

instance : MyInterfaceSpec String where
  getType _ := "String"
  getString s _ := s

instance : MyInterfaceSpec Int where
  getType _ := "Int"
  getString _ h := by
    simp only [String.reduceEq] at h
    -- since `h` says `"Int" = "String"`, we have a contradiction, and don't need to return.
example : List MyInterface := [⟨"test1"⟩,⟨(1:Int)⟩]

[Edward van de Meent]

do note that using a single class for this can get quite out of hand. you'll likely want to define a hierarchy of classes and associated structures, along with (possibly) coersions between the structures

[Edward van de Meent]

it can get out of hand, because when something is of type "MyInterface", you generally only will be able to tell if you have the right type by using functions only depending on the values of MyInterfaceSpec

[Niels Voss]

Out of curiosity, what do you plan on using existential types for? The problem is that in general, deciding whether two types are equal is undecidable (and even worse, if two types have the same cardinality but are derived from different inductive types, then deciding whether two types are equal is actually independent of Lean). So in particular, trying to extract all elements of a type A from a list is uncomputable. (You can actually use the axiom of choice to produce the desired list. This is probably not what you want though, because such a list would be noncomputable and only useful in proofs.)

I think Lean is capable of implementing most of the examples here: https://wiki.haskell.org/Existential_type. Lean can upcast to a typeclass just fine, it just isn't capable of downcasting (or basically doing anything that you would need an instanceof in an object oriented language) without explicitly tagging the types (at least I think, it's possible there's some extra metadata attached to terms that I'm not aware of).

[misterdrgn]

@Niels Voss It's largely a thought experiment. When I look at a new language, I tend to think about how easily I could implement a system from my work (research lab), which was programmed in Clojure. Since Clojure has dynamic typing, getting the system to work in a statically typed language makes for an interesting challenge. One of the trickier bits is supporting a heterogeneous list with upcasting and downcasting. You have a set of components that operate in parallel and produce elements as output. All the elements conform to certain constraints, but their details differ, so you can think of these as being different instances of the same type class. The elements are gathered into a single collection (a heterogeneous list or set), at which point the various components can search through this collection for for elements that meet particular criteria. So that's the point at which you need to downcast; in some cases you might downcast all the way to the concrete type, but in other cases you might downcast to a more specific type class. The final bit is that the system needs to be flexible, as new concrete types (new types of elements) can be added all the time. So that's where shoving everything into an inductive type seems less appealing, although I'm open to it if there's a flexible way to do it that doesn't require adding a bunch of boilerplate for each constructor in the inductive type (see my post at the top of this thread).

I hope that makes sense. Likely, the system could be reimplemented in a new way that removed the need for heterogeneous lists. I'm just curious about what it would take to make that approach work in Lean, or in any statically typed language. (The language where I've had the most success is actually Swift. I think Scala would work well also. These languages are way less finicky about existential types with downcasting than, say, Haskell).

EDIT: Admittedly, my Swift solution uses macros to eliminate boilerplate code. Perhaps that would also be the way to go for Lean. But I appreciate that Swift has easy downcasting.

[Niels Voss]

I totally understand thought experiments trying to figure out what is theoretically possible in a language. To dispel some concerns that downcasting might be completely impossible, there is a function unsafeCast which will reinterpret a value of one type as a value of another type. This is usually a really terrible solution. If you do an invalid cast, it triggers undefined behavior. Also, you can only call this function in an unsafe block, so you can't prove anything about the semantics of programs that use such a function. However, it does exist if you really need it.

As for more practical solutions, the problem is that Lean doesn't really have the concept of a run-time type error. Furthermore (and I might be wrong about this), when a Lean term is compiled down to native code, it is just a stream of bits representing the data, and there is no metadata attached that might allow you to determine the type. This is the same problem that C has, where if you have an array of void * you can't just extract the subarray of elements of a given type.

Language that support things like instanceof usually attach some extra data at run time to make them possible. I think Lean does not do this automatically, so you need to do it manually. You could potentially make a TypeId typeclass which just contains a string, and then use metaprogramming so that you can just write deriving TypeId for Int or something (can't remember the exact syntax) to automatically add an instance of TypeId for a given type. (See SizeOf for a typeclass which is derived on every inductive type).

This approach is imperfect because there's no way to get from the fact that a term has a given string id to a term of the required type. This itself might require unsafeCast, which is bad. The solutions posted above by others will probably work better.

I can elaborate on details or maybe a compromise which works for your specific example later when I have more time.

[misterdrgn]

@Niels Voss I appreciate your response, and I take your point about explicit downcasting not really being a thing in Lean. I do want to explore @Edward van de Meent 's proposed solution, but to be honest there are a lot of bits I don't understand. I may need to spend some more time with the Functional Programming in Lean book, at a minimum (this is where I miss having a full reference manual, so it's nice to hear that's being looked at). The universe u / Type u bit is a complete mystery to me, and I'm also curious what setting autoImplicit to false does.

EDIT: Found the part of the book that discusses universes. Guess I jumped the gun on that one. But I'm lost on the middle part with MyInterface.

[Niels Voss]

Is there a specific topic or topics you want covered in documentation? While Lean's documentation is currently not the best, there's still a fair bit of it, scattered between Theorem Proving in Lean 4, the Lean 4 Manual, and the Mathlib 4 API documentation.

See https://lean-lang.org/lean4/doc/autobound.html for what autoImplicit does. Basically, if autoImplicit is set to true, it will automatically add parameters to your function if it encounters a variable name you haven't defined yet. If autoImplicit is set to false, you may need to use variable or define the parameters explicitly.

autoImplicit has been controversial, because while it makes code less verbose, it also means if you make a typo, your code might compile for now, but not define the function you think you are defining. If I remember correctly, autoImplicit is true by default in Lean, but false if you are working on Mathlib. My recommendation is to always set autoImplicit to false at the top of every file until you get to the point where you can make an informed decision for yourself.

[Niels Voss]

But I'm lost on the middle part with MyInterface.

Basically, an element of MyInterface consists of 1. a type T, 2. an implementation of the typeclass MyInterfaceSpec for T, and 3. an element of type T. Basically, it is just an existential type.

The {} around T : Type u and the [] around toSpec : MyInterfaceSpec T mean that Lean will figure out what to set T and toSpec to for you. Right now, you can create an element of MyInterface like MyInterface.mk "hi" or just ⟨"hi"⟩ . But if the {} and [] were removed from the definition of MyInterface, you would instead have to type out MyInterface.mk String someInstanceOfMyInterfaceSpecForString "hi".

[misterdrgn]

That makes sense on autoImplicit, thanks.

I think useful things in a reference manual would include glossaries/searchable indices for keywords, options that can be set with set_option, and attributes. It would also be cool to have an operator cheat sheet--I found one of those for Haskell, and it was really helpful. I know that many Haskell operators like <$> are also found in Lean, but I tried at least one that wasn't.

Of course, different operators can be defined in different libraries. I'm not entirely clear on the library structure for Lean. I was looking for the standard library, but I think maybe it's the library that's loaded by default, which is also called "init" here: https://leanprover-community.github.io/mathlib4_docs/

Or maybe that's separate from the standard library? And then there's the batteries library, which I guess is part of mathlib, meaning it's community developed?

Those are the kinds of questions I'm running into. A lot of it can be found in those three online books, and I just discovered that those books are searchable, which is nice, but finding the right answer can be difficult.

Just some thoughts, since you asked. I appreciate that the community seems responsive and friendly on here. Really what it comes down to is that for a mature language, you can search online to find answers, since someone else has likely asked your question before. But with a newer language, it helps to have all the answers in one place. My specific question right now is what's happening here:

structure MyInterface where
  {T : Type u}
  [toSpec : MyInterfaceSpec T]
  val : T

attribute [instance] MyInterface.toSpec

Thanks for talking about all this.

EDIT: Just saw your update. So structures can contain type class instances? Crazy.

[Daniel Weber]

Regarding the libraries, if I'm not mistaken:

• There is core, which contains Lean, Init, Std and Lake (lake is Lean's build system, I don't believe it's often used programmatically)
• There is batteries, which is a community-maintained programming library.
• There is Mathlib, which is a community-maintained mathematics library.

• There are some other libraries Mathlib depends on:
  -- Aesop, an automation tactic
  -- ImportGraph, a tool for analyzing imports
  -- ProofWidgets, I believe this is a library for interactive tactics, but I'm not certain
  -- Qq, a library for type-safe metaprogramming

• There are a bunch of other libraries at: https://reservoir.lean-lang.org/

[Mario Carneiro]

If you want runtime type checking, you may also want to consider docs#Dynamic, which is basically a type with a type tag, for which you can implement the getOfType function that Tomas shows

[Mario Carneiro]

def Item := Dynamic

def getValue (α : Type) [TypeName α] (values: List Item): List α :=
  values.filterMap (·.get? α)

deriving instance TypeName for String
deriving instance TypeName for Nat
deriving instance TypeName for Float

#eval getValue String [.mk "hi", .mk "there", .mk 2, .mk 4.5]  -- ["hi", "there"]
#eval getValue Nat [.mk "hi", .mk "there", .mk 2, .mk 4.5] -- [2]
#eval getValue Float [.mk "hi", .mk "there", .mk 2, .mk 4.5] -- [4.500000]

[Tomas Skrivan]

What would be the idiomatic way of bundling Dynamic with a typeclass instance? I.e. achieving runtime polymorphism?

[Mario Carneiro]

Dynamic already uses a typeclass instance

[Mario Carneiro]

note the deriving instance TypeName lines above

[Mario Carneiro]

You should probably not wrap the TypeName instance in another class because TypeName has a deriving handler which does some unsafe things which are hard to replicate without writing manual unsafe code

[Tomas Skrivan]

I probably wasn't clear, what if I want a list where every item is an element of some group. I.e. I want to bundle every list item with an appropriate instance of Group.

[Edward van de Meent]

I'd say that example is likely to run into defeq issues, because even if you do find two elements of the same type, the instances needn't be defeq let alone propeq, so you'll need to choose which multiplication you use when you do.

[Tomas Skrivan]

Maybe Group is not a good example but what about ToString, that would be quite helpful.

[Edward van de Meent]

In that case, the MyInterface approach I suggested some time ago should suffice. (You can make MyInterfaceSpec extend it or some variant of that)

[Mario Carneiro]

Here's a generalization of Dynamic to allow you to store more information than just a value of the target type:

import Mathlib.Data.Real.Basic

open Lean

private opaque PDynamicPointed (P : Type → Type) : NonemptyType.{0} :=
  ⟨Name × NonScalar, inferInstance⟩

/--
Type-tagged union that can store any type with a `TypeName` instance.

This is roughly equivalent to `(α : Type) × TypeName α × P α` but without the
universe bump.
-/
def PDynamic (P : Type → Type) : Type := (PDynamicPointed P).type

instance {P} : Nonempty (PDynamic P) := (PDynamicPointed P).property

private unsafe def PDynamic.typeNameImpl {P} (any : PDynamic P) : Name :=
  (unsafeCast any : Name × NonScalar).1

/--
The name of the type of the value stored in the `Dynamic`.
-/
@[implemented_by PDynamic.typeNameImpl]
opaque PDynamic.typeName {P} (any : PDynamic P) : Name

private unsafe def PDynamic.get?Impl {P} (α) (any : PDynamic P) [TypeName α] : Option (P α) :=
  let ((typeName, obj) : Name × NonScalar) := unsafeCast any
  if typeName == TypeName.typeName α then
    some (unsafeCast obj)
  else
    none

/--
Retrieves the value stored in the `Dynamic`.
Returns `some a` if the value has the right type, and `none` otherwise.
-/
@[implemented_by PDynamic.get?Impl]
opaque PDynamic.get? {P} (α) (any : PDynamic P) [TypeName α] : Option (P α)

private unsafe def PDynamic.mkImpl {α P} [TypeName α] (obj : P α) : PDynamic P :=
  unsafeCast (TypeName.typeName α, (unsafeCast obj : NonScalar))

@[implemented_by PDynamic.mkImpl]
opaque PDynamic.mk {α P} [TypeName α] (obj : P α) : PDynamic P

def Groupish := PDynamic (fun α => AddGroup α × α)

def getValue (α : Type) [TypeName α] (values: List Groupish): List α :=
  values.filterMap (·.get? α) |>.map (fun x => x.2)

def getZero (α : Type) [TypeName α] (values: List Groupish): List α :=
  values.filterMap (·.get? α) |>.map (fun x => x.1.zero)

def Groupish.mk {α} [TypeName α] [g : AddGroup α] (x : α) : Groupish := .mk (g, x)

deriving instance TypeName for Int
deriving instance TypeName for Real

#eval getValue ℤ [.mk (23 : ℤ), .mk (34 : ℝ)]  -- [23]
#eval getValue ℝ [.mk (23 : ℤ), .mk (34 : ℝ)]  -- [Real.ofCauchy (sorry /- 34, 34, 34, 34, 34, 34, 34, 34, 34, 34, ... -/)]
#eval getZero ℤ [.mk (23 : ℤ), .mk (34 : ℝ)]  -- [0]
#eval getZero ℝ [.mk (23 : ℤ), .mk (34 : ℝ)]  -- [Real.ofCauchy (sorry /- 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, ... -/)]

[Mario Carneiro]

It doesn't seem all that useful to have a heterogeneous list of groupish objects though, you can't multiply them together or do much generically with them

[misterdrgn]

@Mario Carneiro Your first code example is exactly what I was looking for. Dynamic.get? looks a lot like downcasting functions I see in other languages. And I like that the boilerplate for applying it to more types is so minimal. I don't know if there are any drawbacks--in some languages people hold their nose at using dynamic types, and you mention there are unsafe operations. But thanks for bringing this up.

I guess the next question would be whether one can build on this. Dynamic provides a single level of abstraction, but suppose you want more. You might have a Circle, which is a Shape, which is an Item. So you start with your List Item, and you might want to find all the instances of Circle, or you might want to find all the instances of Shape, where you expect Shape to support certain methods, such as Shape.boundingBox. This is where tying existential types to type classes, as some languages do, is valuable, as Circle might be an instance of the Shape type class. Perhaps I'll think more on this.

[Mario Carneiro]

This is not very easy, lean basically has no OO-style subtyping system and relies completely on haskell-style typeclasses to do the equivalent. If you wanted to use something like Dynamic for this you would have to encode a computable version of the hierarchy in the tag (Dynamic uses the name of the type as the tag, which is not sufficient for all purposes, especially if there are type operators involved). I think in general this approach is not recommended and you should instead use algebraic types (i.e. inductive) or typeclasses depending on whether you need an open or closed class of types

[misterdrgn]

@Mario Carneiro Yes, understood. This is why I was originally asking about existential types--in some languages, type classes or the equivalent can be use as types in a list or other collection. Haskell supports this with a language extension, but afaik you can't downcast from the existential type in Haskell.

Based on other suggestions in this thread, it sounds like there might be a reasonable type class-based solution in Lean, but it requires a fair amount of boilerplate, far more than the Dynamic version. Perhaps that could be addressed with macros. I haven't looked into Lean macros yet.

In any case, it's largely a thought experiment. I recognize that this is not the way most strongly typed languages are meant to be used.

I appreciate the advice.

[mars0i]

misterdrgn said:

Hi all. I've been reading about Lean4 with great interest, as the syntax largely looks like an improvement on Haskell. I'm interested in playing around with it as a general purpose programming language, rather than doing any math-specific applications. I know Lean is supposed to support general programming, but I see very little information about this (aside from the Functional Programming in Lean book, which is what piqued my curiosity). Is this something that people look at seriously? I recognize that the available libraries would be quite limited. I don't want to do anything crazy for now, probably just some command-line tools.

Since it seems to be a relatively rare interest in the Lean community, I wanted to mention that I'm also interested in Lean as a general-purpose language (and also came from Clojure, via some other dependently typed languages--Idris and Agda.). I like dependent types because they give one more flexibility and control than a language like Haskell--though there are additional complexities as well--and I love how responsive the editing experience is in Lean. It also can be valuable to be able to have the option prove the correctness of parts of a program. (I am interested in the role of dependently typed languages in theorem proving, even if that's not my focus.)

[misterdrgn]

@mars0i I agree that the editing experience is fantastic. It's miles ahead of Haskell, so that's another point in its favor.

[Nicolas Rolland]

A nice paper on OO vs abstract data type of functional programming. This might help you to replace these objects.
On Understanding Data Abstraction, Revisited

[misterdrgn]

@Edward van de Meent I tried to do the following, partially inspired by your code snippet above. The getType implementations failed, apparently because you can't do equality checks on types. Do you know if there's some other way to make getType work with the function signature shown here? I realize I could change the first argument from a Type to a String, but this is less reliable because a developer could get wrong results due to a typo (EDIT: Nm, then it wouldn't know the return type). Or I could try and emulate what Dynamic is doing, but that might get messy. Thanks.

universe u

class Shape (α: Type u) where
  width: α → Nat
  height: α → Nat
  getType: (T : Type) → α → Option T

structure Point where
  x: Int
  y: Int
deriving Repr

instance : Shape Point where
  width _ := 1
  height _ := 1
  getType tp pt := match tp with
  | Point => some pt
  | _ => none

structure Rect where
  x: Int
  y: Int
  width: Nat
  height: Nat
deriving Repr

instance : Shape Rect where
  width := (·.width)
  height := (·.height)
  getType tp rect := match tp with
  | Rect => some rect
  | _ => none