Help on type unification - Implementing a minimal Kyo kernel

Stream: general

[Victor Borja]

Hello,

I'm trying to implement a minimal Kyo kernel to later try help formalizing it.

Flavio Brasil (Kyo's author) kindly provided a gist containing a minimal kernel in Scala3 so I've been studying it and trying to implement it in Lean.

I currently have a very minimal implementation following Flavio's micro-kernel. Currently my proof of concept doesn't even work, it's currently almost a 1-to-1 mapping from Scala to Lean (except from some workarounds given the difference between Scala3 types and Lean) but I'm pretty happy with how the Lean code is getting shaped, but now I'm here to ask for some help involving type inference in Lean4. Once I get the prototype to run correctly, the most interesting work will be in trying to prove termination for kyo's effect handling.

The following is a link to my current code - pasted it into lean4web for sharing -:
Kyo.lean

Note: My lean code tries to use the same conventions and operators as Scala3's Kyo.
So it might be easier to understand if you know a bit about Kyo on Scala.
For example, V < H & P is a computation of value V after H & P effects have been handled. H & P is currently just a list of Pending effects, a naive replacement of Scala3 intersection types.

The problem in my current code (line 90 is red on the type of a suspended value) seems to involve the following data types:

 inductive Effect (V: outParam Type) (P: outParam Pending): Type 1 where
  | Pure (v: V)
  | Suspend {A B: outParam Type} (tag: Tag) (input: A) (cont: B -> Effect V P)

and

class Handler (State X Y: Type) (Eff: Type 1) where
    tag: Tag
    handle: State -> X -> (Y -> Eff) -> State × Eff

Handler.handle is the function that takes a world state, a previously suspended value A and the continuation B -> V < P as given to Effect.Suspend and produces a new state and remaining effect. (At the very bottom there's an Abort effect trying to showcase usage)

Now, the issue (line 90), to me seems to be that currently my code is not able to infer that I want the types A and B from Effect.Suspend to match X and Y as given to Handler.

Even when I'm explicitly providing the types at line 88 for Kyo.Effect.Suspend (A:=X) and also the types for Handler are given explicitly.

However the Lean inspector shows that there are two different X types. I'm not sure where the second one arises from. The variable i, the input value given to Suspend, is unable to unify it's type.

If anyone more well versed than me in how might Lean introduce implicit types, and has any pointer on how to solve my issue, I really would appreciate your help.

[Daniel Weber]

You could try using set_option autoImplicit false to avoid implicit variables altogether

[Sebastian Ullrich]

Now, the issue (line 90), to me seems to be that currently my code is not able to infer that I want the types A and B from Effect.Suspend to match X and Y as given to Handler.

But you're not allowed to do that. A pattern match has to handle all cases, so what is happening is that you're introducing a new X and Y instead of forcing A and B to the existing X and Y.

[Sebastian Ullrich]

outParam also doesn't do anything on inductive so likely this part is an incorrect translation of the Scala type

[Victor Borja]

Replying to self, -while also trying to be more helpful to others- as to why you cant match on a type given to a constructor (as opposed to a type given to a type-constructor as for example Option).

type parameter on constructor will introduce a new type variable

It would be nice to be able to write something like:

  match x with
    | @Foo.bar Nat b => -- b is a Nat
    | Foo.bar b => -- b is anything but a Nat

Update: The following seems to have no problem:

matching on foo

[Victor Borja]

Ok, now after the previous insights, I'm trying the following:

Screenshot 2025-02-09 120153.png

How could I implement head for a heterogeneous list in Lean4 ?

[Victor Borja]

How could I implement head for a heterogeneous list in Lean4 ?

There's an example of an HList on examples/deBruijn.lean, hope that helps :)