Total function not reducing

Stream: lean4

[Locria Cyber]

Hello, everyone. I am making an algebraic effect library.

Eff.lean:

namespace Eff

class inductive Has : {α: Type u} -> α -> List α -> Type u where
| zero : Has x (x::xs)
| succ : Has x xs -> Has x (y::xs)

-- any way to automate this?
instance : Has a (a :: xs) := Has.zero
instance [prev: Has a xs] : Has a (x::xs) := Has.succ prev


inductive Union : List (Type u -> Type v) -> Type u -> Type _ where
| mk : [_prf : Has ε εs] -> (x : ε α) -> Union εs α


example : Union [IO] Unit := Union.mk (IO.println "Hello")
axiom Example_Monad : Type -> Type
example : Union [Example_Monad, IO] Unit := Union.mk (IO.println "Hello")


inductive Free : (_monad: Type u -> Type v) -> (_res: Type u) -> Type _ where
  | pure : α -> Free ε α
  | bind : ε α -> (α -> Free ε β) -> Free ε β

instance : Pure (Free ε) where
  pure := Free.pure

def Free.recurbind (val: Free ε α) (cont: α -> Free ε β) : Free ε β :=
  match val with
  | Free.pure v => cont v
  | Free.bind mval mcont =>
    Free.bind mval (λ a' => Free.recurbind (mcont a') cont)

instance : Bind (Free ε) where
  bind := Free.recurbind


def Eff (es: List (Type u -> Type v)) : (_res: Type u) -> Type _ := Free (Union es)


example : Type 2 := Eff [IO] Nat


def lift [has: Has ε εs] (simple: ε α) : Eff εs α :=
  let un : Union εs α := Union.mk simple
  Free.bind un Free.pure

However, the function Eff above is not reducing.

Main.lean:

import Eff
open Eff

def main_eff : Eff [IO] Unit := do
  lift $ IO.println "hello"
  lift $ IO.println "hello"

error:

Main.lean:5:2

failed to synthesize instance
  Bind (Eff [IO])

[Locria Cyber]

How do I make Eff [IO] reduce to Free (Union [IO])?

[Henrik Böving]

By declaring your definition of Eff as an abbrev or tagging it with @[reducible] (equivalent):

abbrev Eff (es: List (Type u -> Type v)) : (_res: Type u) -> Type _ := Free (Union es)

or

@[reducible]
def Eff (es: List (Type u -> Type v)) : (_res: Type u) -> Type _ := Free (Union es)

[Locria Cyber]

Where can I find all the @[xxxx] "pragma"?

[Locria Cyber]

Also abbrev/lemma/def stuff

[Locria Cyber]

I can't find in tutorial

[Henrik Böving]

In an ideal world we would have a tutorial for all of this already but since we are at a very early stage the answer right now is: by reading other people's code, specifically parts of the Lean compiler and Stdlib as well as Mathlib are sources of good code.

And the alternative is to just ask here.

One could argue that mentioning abbrev in https://leanprover.github.io/theorem_proving_in_lean4/type_classes.html would definitely make sense though since its a very basic thing we do all the time.

[Henrik Böving]

Regarding types of declarations you have already found most though in main Lean we have

• def, abbrev
• axiom
• structure, class
• inductive, class inductive
• axiom
• opaque
• instance
• theorem
• example

and that's all, lemma is a syntactic abbreviation for theorem that is added by mathlib

[Sébastien Michelland]

To clarify, @[reducible] marks the definition as reducible for typeclass inference specifically. By default typeclass inference avoids reducing because it would make the search very expensive.

[Locria Cyber]

what's the different between axiom and opaque

[Locria Cyber]

@Henrik Böving thanks! it works.

[Henrik Böving]

opaque requires you to provide a proof that the type is Inhabited which avoids inconsistencies. axiom can in theory allow you to introduce whatever you want.

[Mac]

Henrik Böving said:

opaque requires you to provide a proof that the type is Inhabited

Technically, it now just requires Nonempty, not Inhabited (with caveats):

opaque Foo : Type
@[instance] axiom Foo.nonempty : Nonempty Foo
unsafe def unsafeFoo : Foo := unsafeCast 0

opaque unimplFoo : Foo -- errors, noncomputable
noncomputable opaque noncomputableFoo : Foo -- works
@[implementedBy unsafeFoo] opaque implFoo : Foo -- works
@[extern c inline "0"] opaque externFoo : Foo -- works

[Locria Cyber]

Mac said:

Henrik Böving said:

opaque requires you to provide a proof that the type is Inhabited

Technically, it now just requires Nonempty, not Inhabited (with caveats):

opaque Foo : Type
@[instance] axiom Foo.nonempty : Nonempty Foo
unsafe def unsafeFoo : Foo := unsafeCast 0

opaque unimplFoo : Foo -- errors, noncomputable
noncomputable opaque noncomputableFoo : Foo -- works
@[implementedBy unsafeFoo] opaque implFoo : Foo -- works
@[extern c inline "0"] opaque externFoo : Foo -- works

I'm new to Lean. I have to remember all these keywords? :rolling_on_the_floor_laughing:

[Henrik Böving]

It gets easier over time :p and most of what he showed isn't relevant to everyday Lean don't worry

[Locria Cyber]

what the different between def and theorem?

[Locria Cyber]

Also, is there something like go or let ([a 1] [b 2]) body in lisp for inline recursion?

[Henrik Böving]

a theorem is always of type P where P : Prop, a def can be whatever.

inline recursion:

def iotaTR (n : Nat) : List Nat :=
  let rec go : Nat → List Nat → List Nat
    | 0, r => r.reverse
    | m@(n+1), r => go n (m::r)
  go n []

like this?

[Locria Cyber]

yes

[Locria Cyber]

How do I turn anything into a string

[Locria Cyber]

Sort and Type has any difference?

[Henrik Böving]

we have the docs4#ToString typeclass to turn stuff into strings, we have docs4#Repr for "debug representation" of data structure basically and we have format strings like: s!"Lalalala {variable} lalalalala"

There is an infinite hierarchy of types, we have

1. Prop at the bottom where Prop is equivalent to Sort 0
2. Type which is equivalent to Sort 1
3. Type 1 which is equivalent to Sort 2
   and so on until infinity. The hierarchy exists in order to avoid self reference paradoxa

[Locria Cyber]

Prop is Sort 0?

[Locria Cyber]

I don't quite understand

[Henrik Böving]

Yes, they are aliases for each other

[Henrik Böving]

you can even ask Lean about this:

example : Sort 0 = Prop := by rfl
example : Sort 1 = Type := by rfl
example : Type u = Sort (u+1) := by rfl

[Locria Cyber]

What exactly is Prop?

[Locria Cyber]

There is also the difference between computable subset of Type 0 and "incomputable" Type 0

[Locria Cyber]

What exactly is Prop?

[Kyle Miller]

If x : p, y : p, and p : Prop, then x = y is true by rfl ("proof irrelevance") and there are also some special rules for universe levels when Prop is involved ("impredicativity" I believe?). It's meant to represent the universe of mathematical Propositions.

[Henrik Böving]

It is the type of mathematical Properties. So everything that we want to express as a logical statement in Lean has type Prop, equalities, inequalities, statements about correctness of certain functions etc.

[Henrik Böving]

In general if you have some statement p where p : Prop and you provide a value h : p what you have done is create a proof that p does indeed hold, this is the principle of how proofs work in Lean. What Kyle is describing above is a certain special property of Prop in Lean which says that if we have two proofs of the same statement we can always consider those proofs equivalent (it helps with code generation efficiency)

[Kyle Miller]

I suppose Prop's special properties were originally motivated by codegen, but it seems to be important for doing classical mathematics (like it's possible to define Subtype with the correct cardinality).

[Kyle Miller]

There's another thing about Prop that's special, which is its elimination rules -- in contrast to Type, they prevent you from getting data out of a proposition.

[Kyle Miller]

(It seems people have found this diagram to be useful, so here's a link.)

[Kyle Miller]

This page about foundations mentions everything I've mentioned about Prop.

[Locria Cyber]

What's the constructor for Prop?
Only _=_?

[Reid Barton]

No there are lots of ways to construct propositions, just like there are lots of ways to construct types.

[Henrik Böving]

No you are mis understanding, just like you can declare your own things in Type (Nat, String etc.) you can also declare your own things in Prop via inductive and structure, docs4#Eq, docs4#Nat.le etc.

[Locria Cyber]

So it's a black box?

[Locria Cyber]

I use Idris more and there is no such thing as Prop in Idris. The equality type Equal a is like inductive in Lean

[Locria Cyber]

Main> :doc Equal
Prelude.Equal : Prec
data Builtin.Equal : a -> b -> Type
  Totality: total
  Visibility: public export
  Constructor: Refl : x = x
  Hints:
    Equivalence ty Equal
    Euclidean ty Equal
    PartialEquivalence ty Equal
    Reflexive ty Equal
    Symmetric ty Equal
    Tolerance ty Equal
    Transitive ty Equal

[Henrik Böving]

Our equality type is also an inductive in Lean as I linked above: docs4#Eq it is just that we gave our mathematical propositions a special place to live in for the reasons outlined above

[Locria Cyber]

Kyle Miller said:

There's another thing about Prop that's special, which is its elimination rules -- in contrast to Type, they prevent you from getting data out of a proposition.

So Prop don't increase the universe level by one?

[Locria Cyber]

Locria Cyber said:

Eff.lean:

namespace Eff

class inductive Has : {α: Type u} -> α -> List α -> Type u where
| zero : Has x (x::xs)
| succ : Has x xs -> Has x (y::xs)

-- any way to automate this?
instance : Has a (a :: xs) := Has.zero
instance [prev: Has a xs] : Has a (x::xs) := Has.succ prev


inductive Union : List (Type u -> Type v) -> Type u -> Type _ where
| mk : [_prf : Has ε εs] -> (x : ε α) -> Union εs α


example : Union [IO] Unit := Union.mk (IO.println "Hello")
axiom Example_Monad : Type -> Type
example : Union [Example_Monad, IO] Unit := Union.mk (IO.println "Hello")


inductive Free : (_monad: Type u -> Type v) -> (_res: Type u) -> Type _ where
  | pure : α -> Free ε α
  | bind : ε α -> (α -> Free ε β) -> Free ε β

instance : Pure (Free ε) where
  pure := Free.pure

def Free.recurbind (val: Free ε α) (cont: α -> Free ε β) : Free ε β :=
  match val with
  | Free.pure v => cont v
  | Free.bind mval mcont =>
    Free.bind mval (λ a' => Free.recurbind (mcont a') cont)

instance : Bind (Free ε) where
  bind := Free.recurbind

In this case, I do need to take data out of Has e es though.

I need to take stacked monad apart to handle algebraic effects, and _prf in Union.mk is the position that I need to use.

In a sense, I need to pattern match Has e es, but it's never shown to the user.

[Mac]

Henrik Böving said:

a theorem is always of type P where P : Prop, a def can be whatever.

Technically, a theorem can be of any type:

theorem foo : Nat := 5 -- ok

I believe a theorem is essentially a noncomputable def (just with some syntactic sugar on top) :

theorem foo : Nat := 5
def addFoo (x : Nat) : Nat := x + foo
/-
error:
failed to compile definition, consider marking it as 'noncomputable'
because it depends on 'foo', and it does not have executable code
-/
noncomputable example (x : Nat) : Nat := x + foo -- ok

However, Henrik is right in spirit. We generally use a theorem for proposition we want to prove and a def for encoding concepts and generating code. I just enjoy demonstrating edge cases. :big_smile:

[Mario Carneiro]

Actually I think it's a noncomputable opaque