can you do a safe cast to a subtype in Lean?

Stream: lean4

[Chris Lovett]

Can lean 4 do something like this?

structure Command where
  name : string

structure RunnableCommand extends Command where
  run : (List String) -> IO UInt32

def runIt (cmd : Command) : IO UInt32 :=
  match cmd with
  | RunnableCommand c => c.run []
  | _ => IO.println "Not runnable"
  return 1

[Sebastian Ullrich]

You misunderstand inheritance, it is merely a shortcut for structural composition. Lean is not an object-oriented language, it does not have subtypes.

[Sebastian Ullrich]

For a constant number of "subclasses" known in advance (a "clossed class" in some languages), we usually model them as different constructors of an inductive data type instead.

[Yuri de Wit]

I had a similar question come up when looking into Julia's multiple dispatch in Lean4 using type classes (static vs dynamic aside):

def doSomething(cmd : Command) := ...

#eval doSomething (RunnableCommand.mk  ...)

In theory, a simple automatic coercion could make this work, no?

[Sebastian Ullrich]

That's the opposite casting direction, but yes, it can