Error with inductive

Stream: new members

[Miguel Negrão]

I'm trying to translate the following haskell code

data MSF m a b = MSF { unMSF :: a -> m (b, MSF m a b) }

to lean. My attempt below causes an error.

inductive MSF (m : Type u → Type u) (a b : Type u) : Type u where
  | mk : (a → m (b × MSF m a b)) → MSF m a b

(kernel) arg #5 of 'MSF.mk' contains a non valid occurrence of the datatypes being declared

Can anyone help with this error ? If I remove m from mk it works...

[Eric Wieser]

The #lean4 > Free monad thread sounds quite similar

[Eric Wieser]

The quick fix is to add unsafe, the right fix is probably more involved. What does MSF stand for here?

[Kyle Miller]

MSF is not allowed because if there were such a type you could create an element of Empty.

unsafe inductive MSF (m : Type u → Type u) (a b : Type u) : Type u where
  | mk : (a → m (b × MSF m a b)) → MSF m a b

unsafe def mkEmptyOf : MSF (· → Empty) Unit Unit → Empty
  | .mk f => f () ((), .mk f)

unsafe def mkEmpty : Empty :=
  mkEmptyOf <| MSF.mk (fun () => fun ((), m) => mkEmptyOf m)

I think this is basically using the omega/y-combinator trick to get an infinite loop even without an obvious recursion.

[Miguel Negrão]

Thanks Eric and Kyle. Ok, so it seems MSF cannot safely be defined in lean4. My ideia here was to practice doing proofs, so unsafe doesn't help.

MSF stands for Monadic Signal Function, and it is a recent approach to Functional Reactive Programming. The paper that introduces it is here in pdf. It is implemented in the dunai Haskell library, and the definition of MSF is here.

MSF is an update on Arrowised FRP, of which the prime example is Yampa, which, optimizations aside, has as core data element type SF ′ a b = DTime → a → (b, SF ′ a b) which appears to work ok in lean:

inductive SF (a b : Type u) : Type u where
  | mk : (Float → a → (b × SF a b)) → SF a b

So the main problem appears to be the presence of the monad m.

The fact that when evaluating the MSF or SF you get to generate a new MSF or SF means that you can hide state in the signal function, and it also means the behaviour of the signal function can change radically when some particular event appears.

I'll keep exploring the Free Monad thread, and if nothing works, I'll just play with SF.

[Miguel Negrão]

I get an interesting error defining the identity SF:

def SF.id {a : Type _} : SF a a := mk (λ t a => (a, SF.id))

fail to show termination for
  SF.id
with errors
structural recursion cannot be used

well-founded recursion cannot be used, 'SF.id' does not take any (non-fixed) arguments

But I'm not actually calling SF.id again in the definition of the function, I'm just providing itself in the result, to be called at some later point. Since the function is not called, shouldn't this not have any issues with termination ?

[Kyle Miller]

I guess this type is empty, so that's a strong reason why you can't define anything. I simplified the type a little by specializing to Unit since there was a termination-by I wasn't sure how to do in SF'.elim when you have b × SF a b.

-- setting a = b = Unit and simplifying
inductive SF' : Type where
  | mk : (Float → SF') → SF'

def SF'.elim {α : Type _} : SF' → α
  | mk f => elim (f 0)

def SF'.equiv : SF' ≃ Empty where
  toFun := SF'.elim
  invFun := Empty.elim
  left_inv := fun x => (x.elim : Empty).elim
  right_inv := fun x => x.elim

[Kyle Miller]

@Miguel Negrão I'm not very familiar with them, but maybe SF is better modeled as a coinductive type rather than an inductive type (it seems like an infinite stream vs a finite tree). Lean doesn't natively have these, but I believe I've heard that there are ways to simulate them regardless. I haven't read it too carefully, but here's what appears to be a previous discussion for a very similar type.

[Miguel Negrão]

@Kyle Miller thanks for pointing me to that discussion. Indeed in that discussion they are trying to implement something similar to Yampa, which is what I was also trying to do, so I will have a look at that. Thanks !

[Miguel Negrão]

this page about the same issue in coq is very illuminating, regarding why it's so easy to define infinite data structures in Haskell, but one has to be very careful with that in theorem provers.