Replicating ML-style modules with classes / structures

Stream: lean4

[George Pîrlea]

Hi. I am converting a FStar module to Lean and looking for advice on the best way of representing it.

The original module looks like this:

module Foo
val concrete_st : Type0
val app_op_t : eqtype
type op_t = pos & (nat & app_op_t)
val app (s:concrete_st) (o:op_t) : concrete_st
end Foo

In Lean terms op_t is an abbrev that depends on the fields of Foo.

Something like this does not work:

mutual
class Foo where
  concrete_st : Type
  app_op_t : Type
  app (s : concrete_st) (op : op_t) : concrete_st

abbrev Foo.op_t {self : Foo} := Nat × (Nat × self.app_op_t)
end
-- invalid mutual block: either all elements of the block must be
-- inductive/structure declarations, or they must all be definitions/theorems/abbrevs

The Foo class will have many other fields that depend on op_t, so it's cumbersome to inline the definition everywhere, and using a macro for this seems weird.

What's the best way to represent this in Lean?

[Shreyas Srinivas]

class Foo  where
  concrete_st : Type
  app_op_t : Type
  op_t := Nat × (Nat × app_op_t)
  app (s : concrete_st) (op : op_t) : concrete_st

[Robin Arnez]

No, that'd make op_t a field with a default value

[Shreyas Srinivas]

Isn't that the intent?

[Robin Arnez]

I thought it should be fixed to Nat x Nat x app_op_t?

[Robin Arnez]

I would've done

class Foo where
  concrete_st : Type
  app_op_t : Type
  app' (s : concrete_st) (op : Nat × Nat × app_op_t) : concrete_st

abbrev Foo.op_t [Foo] := Nat × (Nat × app_op_t)
abbrev Foo.app [Foo] (s : concrete_st) (op : op_t) : concrete_st := app' s op

instead

[Shreyas Srinivas]

Then you must define it for an arbitrary instance

[Robin Arnez]

Hmm what do you mean?

[Shreyas Srinivas]

Right this makes more sense
Robin Arnez said:

I would've done

class Foo where
  concrete_st : Type
  app_op_t : Type
  app' (s : concrete_st) (op : Nat × Nat × app_op_t) : concrete_st

abbrev Foo.op_t [Foo] := Nat × (Nat × app_op_t)
abbrev Foo.app [Foo] (s : concrete_st) (op : op_t) : concrete_st := app' s op

instead

[Shreyas Srinivas]

The original example makes no sense to me because it looks like the you want to either have a default value for the type op_t or impose a constraint that op_t = Nat x (Nat x app_op_t)

[Shreyas Srinivas]

Otherwise, saying Foo.<field> = <val> makes no sense because a field belongs to an instance of the class

[Sebastian Ullrich]

A variant that is close to the original code is

class FooBase where
  concrete_st : Type
  app_op_t : Type

abbrev FooBase.op_t [FooBase] := Nat × (Nat × app_op_t)

open FooBase

class Foo extends FooBase where
  app (s : concrete_st) (op : op_t) : concrete_st

Of course this whole module style is not very prevalent in Lean but I am always interested to hear how it works out and if there are any remaining elaboration issues with it

[George Pîrlea]

That's very helpful. Thank you, everyone!

@Sebastian Ullrich's suggestion is the closest to what I intended. I'll try it out and see how far it gets me.

[Shreyas Srinivas]

Glad to hear it. @Robin Arnez : To describe my issue more succinctly, I think we don't have a concept of associated types like rust do we?