PSBP, a program specification based programming library

Stream: general

[Luc Duponcheel]

Hello Lean folks,

I am Luc Duponcheel, a Functional Programming veteran. I am new to this forum.

I have worked on Monads and Monad Transformers since the 90-ties (previous century) with researchers like Erik Meijer, Graham Hutton, Mark P. Jones, Doaitse Swierstra and others ... .

I am retired now.

I think of a (various) monads as specifications of effectful expressions.

But what are specifications of effectful functions?

Arrows are an appropriate candidate.

I consider, what I call programs as being an appropriate candidate (they are inspired by Backus's FP).

I have implemented a PSBP Scala and Haskell librariy using this idea.
PSBP stands for Program Specification Based Programing.

Recently I decided to also use Lean as a programming language because of its theorem proving capabilities.

Attached (PSBP.lean) you can find preliminary code with my idea's. In practice, PSBP defines a library level, specification based, programming language.

The code is really only the tip of a huge iceberg (no laws and proofs yet, no effects yet, and only 1 trivial active materialization). My Scala and Haskell code is much more elaborated.

I am wondering if I could start some library project to contribute to this community, and, of course, I am wondering if there are any enthusiasts willing to contribute to that project.

Finally, why considering programs (effectful function specifications) instead of computations (effectful expression specifications)? Well, just like functions, programs are denotational artifacts (they have a meaning), while, just like expressions, computations are operational artifacts. Just like functions can be defined using expressions, programs can be materialized using program implementations in terms of computations. I consider functions and programs as a "goal" and expressions and computations as a "means" to reach that goal.

[Luc Duponcheel]

By the way, I aleady have a first remark on the implementation of Applicative. It contains the following definition : seq : {α β : Type u} → f (α → β) → (Unit → f α) → f β. Ok, I understand that, because Lean evaluation is strict, type Unit → f α is used, but why not using Thunk (f α) in order to avoid multiple evaluations?

[Shreyas Srinivas]

Hi Luc, welcome to Lean. I am browsing through your file and in my initial skim, I notice that you could use the inbuilt Prod and Sum types instead of the ProductType and SumType definitions. They will save you a lot of time later when proving theorems. Another quibble. You could share code more easily on this zulip, either through a code block like so:

```
-- some lean code
```

or a github gist. You can make the codeblock collapsible by wrapping it as a spoiler

[Shreyas Srinivas]

This helps us in two ways. First we can copy and paste the code in our editor. Secondly, we can use a little icon on the top right corner of the code block to open it on the lean scratch pad online. You can see this in the example below. The icons appear when you hover the mouse on the code block

def example_code := 37

[Shreyas Srinivas]

Once my laptop finishes updating I will paste a more lean-style refactoring of your code. I think it should make it neater

[Shreyas Srinivas]

At a conceptual level, I see that you are using several typeclass instances again and again. You could also define mixin type classes to extract the common combinations into one typeclass

[Shreyas Srinivas]

Code listing

--
-- generic, specification related, structures
--

-- abbrev ProductType := Prod -- Not required

-- thunks are used because Lean does not fully support lazy evaluation
-- SumType arguments should not both be evaluated
-- abbrev SumType (a b : Type u) := Thunk a ⊕ Thunk b

def foldSum (c2a : c → a)(b2a : b → a)(sum : Thunk c ⊕ Thunk b): a :=
  match sum with
  | .inl tc => c2a tc.get
  | .inr tb => b2a tb.get


-- clowns to the left
-- jokers to the right
def trueToLeftFalseToRightF(zb : a × Bool): Thunk a ⊕ Thunk a :=
  match zb.snd with
    | true => .inl zb.fst
    | false => .inr zb.fst
--
-- specifications
--

-- functions are programs
class Functional (program : Type u → Type u → Type v):
  Type (max (u+1) v) where
    function {a b : Type u} : (a → b) → program a b

export Functional (function)

-- the identity function is a program
def identity [Functional program]: program a a :=
  function id

-- functions can act upon programs
class Functorial (program : Type u → Type u → Type v):
  Type (max (u+1) v) where
    andThenF {a b c : Type u} : program a b → (b → c) → program a c

-- programs can act upon themselves (i.e. programs be (sequentially) composed)
class Sequential (program : Type u → Type u → Type v):
  Type (max (u+1) v) where
  andThen {a b c : Type u} : program a b → program b c → program a c

export Sequential (andThen)

-- programs can create product values
class Creational (program : Type u → Type u → Type v):
  Type (max (u+1) v) where
  product {a b c : Type u}:
    program a b → program a c → program a (b × c)

export Creational (product)

-- programs can create intermediate values
def let_
  [Functional program] [Sequential program] [Creational program]:
    program a b → (program (a × b) c → program a c) :=
      fun (a2b ab2c) => andThen (product identity a2b) ab2c

-- programs can consume sum values
class Conditional (program : Type u → Type u → Type v):
  Type (max (u+1) v) where
  sum {a b c : Type u} : program c a → program b a → program (Thunk c ⊕ Thunk b) a

export Conditional (sum)

-- programs can perform conditional logic
def if_
  [Functional program] [Sequential program] [Creational program] [Conditional program]:
    program a Bool → program a b → program a b → program a b :=
      fun (a2b la2b ra2b) =>
        let_ a2b (andThen (function trueToLeftFalseToRightF) (sum la2b ra2b))

-- trivial library level keywords
-- that are introduced for for esthetic reasons
def in_ : a → a := id

def else_ : a → a := id

--
-- generic, implementation related, structures
--

structure FromComputationValuedFunction
  (computation : (Type u → Type u)) (a b : Type u) : Type (u+1) where
    toComputationValuedFunction : a → computation b

--
-- generic
-- Functional, Functorial, Creational, Sequential, Conditional
-- implementations
--

instance [Applicative computation]:
  Functional (FromComputationValuedFunction computation) where
    function := fun a2b => ⟨fun a => pure $ a2b a⟩

instance [Functor computation]:
  Functorial (FromComputationValuedFunction computation) where
    andThenF := fun ⟨a2cb⟩ b2c =>
      ⟨fun a => b2c <$> a2cb a⟩

instance [Applicative computation]:
  Creational (FromComputationValuedFunction computation) where
    product := fun ⟨a2cb⟩ ⟨a2cc ⟩ =>
      ⟨fun a => pure Prod.mk <*> a2cb a <*> a2cc a⟩

instance [Monad computation]:
  Sequential (FromComputationValuedFunction computation) where
    andThen := fun ⟨a2cb⟩ ⟨b2cc⟩ =>
        ⟨fun a => a2cb a >>= b2cc⟩

instance:
  Conditional (FromComputationValuedFunction computation) where
    sum := fun ⟨c2ca⟩ ⟨b2ca⟩ =>
        ⟨foldSum c2ca b2ca⟩


--
-- specific
-- Functor, Applicative, Monad
-- implementations
--

-- trivial Active implementation
structure Active (a : Type u) : Type u where
  runActive : a
deriving Repr

instance: Functor Active where

  map : {a b : Type} → (a → b) → Active a → Active b :=
    fun a2b ⟨a⟩ => ⟨a2b a⟩

instance: Applicative Active where

  pure : {a : Type} → a → Active a :=
    fun a => ⟨a⟩

  seq : {a b : Type} → Active (a → b) → (Unit → Active a) → Active b :=
    fun ⟨a2b⟩ u2aa => ⟨a2b ( (u2aa ()).runActive )⟩

 instance: Monad Active where

  bind : {a b : Type} → Active a → (a → Active b) → Active b :=
    fun ⟨a⟩ a2ab => ⟨(a2ab a).runActive⟩

--
-- specific implementation based materializations
--

-- trivial Active materialization
def materializeActive: FromComputationValuedFunction Active a b → (a → b) :=
  fun ⟨a2ab⟩ => fun a => (a2ab a).runActive

--
-- primitive examples
--

def isZeroF: Nat → Bool := fun a => a == 0

def isZero [Functional program]: program Nat Bool :=
  function isZeroF

def isOneF: Nat → Bool := fun a => a == 1

def isOne [Functional program]: program Nat Bool :=
  function isOneF

def oneF: Nat → Nat := fun _ => 1

def one[Functional program]: program Nat Nat := function oneF

def minusOneF: Nat → Nat := fun a => a - 1

def minusOne[Functional program]: program Nat Nat :=
  function minusOneF

def minusTwoF: Nat → Nat := fun a => a - 2

def minusTwo[Functional program]: program Nat Nat :=
  function minusTwoF

def addF: Nat × Nat → Nat :=
  fun ⟨a,b⟩ => a + b

def add [Functional program]: program (Nat × Nat) Nat :=
  function addF

def multiplyF: Nat × Nat → Nat :=
  fun ⟨a,b⟩ => a * b

def multiply [Functional program]: program (Nat × Nat) Nat :=
  function multiplyF

--
-- composite (recursive) examples
--
-- 'unsafe' keyword is used because Lean (strangely enough)
-- checks termination of (abstract) program specifications instead
-- of only checking (concrete) program implementation based materializations
--

unsafe def fibonacci
  [Functional program]
  [Creational program]
  [Sequential program]
  [Conditional program]:
    program Nat Nat :=
      if_ isZero one $
        else_ $
          if_ isOne one $
            else_ $
              andThen
                (product
                  (andThen minusOne fibonacci)
                  (andThen minusTwo fibonacci))
                add

unsafe def factorial
  [Functional program]
  [Creational program]
  [Sequential program]
  [Conditional program]:
    program Nat Nat :=
      if_ isZero one $
        else_ $
          let_ (andThen minusOne factorial) $
            in_ $
              multiply

--
-- let's evaluate
--

#eval (materializeActive fibonacci) 10

#eval (materializeActive factorial) 10

-- $ lean PSBP.lean
-- 89
-- 3628800

[Shreyas Srinivas]

1. I have replaced ProductType with Prod. The notation for Prod a b is a × b. The cross is in unicode and written with the shortcut \x.
2. I have replaced SumType with Sum. The notation for Sum a b is a ⊕ b. In this case I have replaced all occurrences of SumType a b with Thunk a ⊕ Thunk b
3. For every structure structure XYZ, you can construct and destructure it as XYZ.mk <field 1> <field 2> .... There is standard notation for this ⟨<field1>, <field2>,...⟩. The left and right arrow brackets are unicode characters respectively written using the shortcuts \< and \>
4. I have replaced all ascii arrows -> with unicode arrows → which can be entered using the shortcuts \-> or \r
5. I have replaced all occurrences of fun a => a with id
6. There was one occurrence of a function creating a product type object from its pieces which looked like fun x y => {fst := x, snd := y}. I replaced it with Prod.mk which does the same thing

[Shreyas Srinivas]

and finally, I have to ask one question : Why do you believe it will be easier to reason with Arrow computations over Monads (for which a system is already being tested in one of the release candidate toolchains)

[Aaron Liu]

Why thunks?

[Luc Duponcheel]

Shreyas Srinivas, thanks so much for your constructive comments. My main goal is to extend my "library level programming language" with extra monad-like features and to establish "program" laws and proof them making use of the corresponding monad laws (I am going to name the various combinations of my type classes "programs" i.e. effectful functions, just like computations (monads) are effectful expressions). Question: In Haskell there is an actor-like library (hakka) to deal with parallelism. I could use that library to add a "parallel product" and, for example, use it to write a parallelFibonacci. Does Lean also have such a library? FWIW, I am just beginning to learn how to write proofs, so do not expect things to proceed very quickly. All comments are welcome.

[Shreyas Srinivas]

I don’t think there is a Hakka style library for parallelism yet

[Shreyas Srinivas]

Cc : @Henrik Böving about parallelism

[Luc Duponcheel]

Aaron Liu, in
sum {a b c : Type u} : program c a → program b a → program (Thunk c ⊕ Thunk b)
only one of the two arguments of the resulting program are supposed to be used. Since, by default, Lean has eager evaluation, I use thunks to emulate lazy evaluation.
by the way, my question about the Applicative interface still remains in
seq : {α β : Type u} → f (α → β) → (Unit → f α) → f β
the (Unit → f α) does not really emulate lazy evaluation (evaluate zero times or one time), but rather "by name evaluation" (evaluate zero or more times). So I think that
seq : {α β : Type u} → f (α → β) → Thunk (f α) → f β
would be more efficient.

[Shreyas Srinivas]

you can get asynchrony using docs#Task

[Henrik Böving]

Shreyas Srinivas said:

Cc : Henrik Böving about parallelism

I work on async IO, not parallelism, these matters are disjoint for the most part.

[Shreyas Srinivas]

Arrows can also represent asynchrony iirc

[Luc Duponcheel]

Shreyas Srinivas can you help me a bit by sending me a private message and copy/paste your first reply into a file that you attach, so that I can see how you produced the collapsed inline code? thx

[Shreyas Srinivas]

I am currently on my phone so this will be difficult for now. But you can open the code in the lean4 playground. If you hover your mouse over the listing you will see two icons on the top right corner. Clicking on one of them will open the code in a lean editor on the web browser.

[Aaron Liu]

Luc Duponcheel said:

Aaron Liu, in
sum {a b c : Type u} : program c a → program b a → program (Thunk c ⊕ Thunk b)
only one of the two arguments of the resulting program are supposed to be used. Since, by default, Lean has eager evaluation, I use thunks to emulate lazy evaluation.
by the way, my question about the Applicative interface still remains in
seq : {α β : Type u} → f (α → β) → (Unit → f α) → f β
the (Unit → f α) does not really emulate lazy evaluation (evaluate zero times or one time), but rather "by name evaluation" (evaluate zero or more times). So I think that
seq : {α β : Type u} → f (α → β) → Thunk (f α) → f β
would be more efficient.

In a sum type, you only get one of the two? program is a function type, so those won't be evaluated until you feed them an argument. And the sum type Thunk c ⊕ Thunk b contains only one thunk in total, and you're forcing it immediately once you acquire it, so I don't see the point of thunks here.

[Aaron Liu]

It would be equivalent to just force the thunk at the call site I think

[Luc Duponcheel]

Shreyas Srinivas, about your final question,
1) short specific answer: Take the associativity law for computations (monads), for programs (btw, you called mine arrows, but they are slightly different) it boils down to
p ~~> (q ~~> r) = (p ~~> g) ~~> r which is so much simpler and intuitive than the corresponding computation law.
2) short general answer: embrace simplicity that is what abstraction is all about.
3) longer answer: computations (monads) are effectful expression specifications, programs are effectful function specifications. Programs and functions are denotational artifacts (they mean something and can be given a meaningful name). Computations and expressions are essentially operational artifacts. For example: can you give a meaningful name to 1 + 2*3 (of course 7 would be a reasonable answer, but you know what I mean). Finally, functions are defined in terms of expressions, likewise programs are defined in terms of computations (that is exactly what I did in my code). Writing programs is the goal using computations for doing so is a means to reach that goal.

[Luc Duponcheel]

Shreyas Srinivas, one final remark. I had to annotate my fibonacci and factorial code with unsafe. Fair enough that Lean does this termination check. But, as I wrote, fibonacci and factorial are not programs, they are program specifications (as can easily be derived by their signature, there are type class constraints involved). I can materialize them in various safe ways (I used Active but I could, e.g. have used Reactive as well, useful for parallelism). Think of a program specification as a (special) kind of program description. Compare this with the painting "Ceci n'est pas une pipe" painted by René Magritte (also from Belgium, just like me). It is a description of a pipe. Or think about a painting with an effect (an explosing bomb), well, luckily enough it is not an explosing bomb so it is not unsafe at all to hang it on your wall.

[Shreyas Srinivas]

If you have termination issues, then marking your code partial should do the trick. The issue here is not one of termination. Lean cannot prove that the type you have specified should be inhabited

[Shreyas Srinivas]

In particular, lean is not sure that program is a non-empty type in the first place.

[Shreyas Srinivas]

So what you need is a Nonempty instance. I added one to the factorial example and now it compiles:

partial def factorial
  [∀ x y, Nonempty (program x y)]
  [Functional program]
  [Creational program]
  [Sequential program]
  [Conditional program]:
    program Nat Nat :=
      if_ isZero one $
        else_ $
          let_ (andThen minusOne factorial) $
            in_ $
              multiply

[Shreyas Srinivas]

but when you invoke it, you have to supply this nonempty instance

[Shreyas Srinivas]

But since you say you are interested in the theorem proving aspects, you should know that there is limited support for proving anything about partial defs

[Shreyas Srinivas]

The existing support goes through something called partial_fixpoint which is currently only supported for functions which return an Option value.

[Luc Duponcheel]

Shreyas Srinivas, you are my hero!

I will update my code, add operation symbols (for readability) and post everything using your instructions on how to do so in an appropriate way.

About the theorem proving aspects ... not really good news to hear about this.

Do you think that refactoring my code using partial_fixpoint and Option results is worth the trouble?

I can imagine that those fixed points are akin to catamorphisms (I used them in the 90-ties when I worked in Utrecht with the group of Erik Meijer) but somewhat modified to yield an Option result in order to transform a partial function into a global one, right?

[Luc Duponcheel]

Thanks for all the constructive remarks.

I updated the code a little bit (I also added a few operation symbols for readability). For now I still use the unsafe keyword. The partial fixed point stuff is for later.

For those who read the factorial definition and wonder what is happening behind the scenes. let_ ... in_ ... creates (Creational) an intermediate local value that, together with the recursive call of minusOne >=> factorial can be used by multiply.

Operationally, instead of popping an argument from the stack and pushing a result on the stack (what happens with sequential composition (Sequential) >>>), it keeps the argument on the stack and pushes the result on top of it on the stack.

My library level programming language is pointfree (cfr. Backus FP), but it can also deal with effects (internal, e.g. state, and external, e.g. IO). The language can also be (and sometimes has to be) used positionally by accessing values on the stack above by position. This is typically necessary for simple sequential main-like programs (think of them as recipes) where, apart from initial ingredients, also intermediate produced ingredients need to be used. Note that the intermediate ingredients can, potentially, be produced by fully fledged programs (for example using recursion and condition (Conditional) to mix appropriate ingredients until they turn into "mayonnaise"). In other words, PSBP supports hybrid pointfree and positional programming. I hope that this analogy helps. Below is the code. Of course it is only the tip of a huge iceberg. My Haskell and Scala code is more elaborate.

Code listing

--
-- generic, specification related, functions
--

def foldSum (c2a : c → a)(b2a : b → a)(sum : Thunk c ⊕ Thunk b): a :=
  match sum with
  | .inl tc => c2a tc.get
  | .inr tb => b2a tb.get


-- clowns to the left, jokers to the right (function)
def trueToLeftFalseToRightF(ab : a × Bool): Thunk a ⊕ Thunk a :=
  match ab.snd with
    | true => .inl ab.fst
    | false => .inr ab.fst

--
-- specifications
--

-- functions are programs
class Functional (program : Type u → Type u → Type v):
  Type (max (u+1) v) where
    function {a b : Type u} : (a → b) → program a b

export Functional (function)

-- the identity function is a program
def identity [Functional program]: program a a :=
  function id

-- functions can act upon programs
class Functorial (program : Type u → Type u → Type v):
  Type (max (u+1) v) where
    andThenF {a b c : Type u} : program a b → (b → c) → program a c

-- programs can create product values
class Creational (program : Type u → Type u → Type v):
  Type (max (u+1) v) where
  product {a b c : Type u}:
    program a b → program a c → program a (b × c)

-- trivial library level keyword
-- introduced for esthetic reasons
def in_ : a → a := id

export Creational (product)

infixl:60 " &&& " => product

-- programs can act upon themselves
-- (programs be (sequentially) composed)
class Sequential (program : Type u → Type u → Type v):
  Type (max (u+1) v) where
  andThen {a b c : Type u} : program a b → program b c → program a c

export Sequential (andThen)

infixl:50 " >=> " => andThen

-- programs can create intermediate values
def let_
  [Functional program] [Sequential program] [Creational program]:
    program a b → (program (a × b) c → program a c) :=
      fun (a2b ab2c) => identity &&& a2b >=> ab2c

-- programs can consume sum values
class Conditional (program : Type u → Type u → Type v):
  Type (max (u+1) v) where
  sum {a b c : Type u} :
    program c a → program b a → program (Thunk c ⊕ Thunk b) a

export Conditional (sum)

infixl:55 " ||| " => sum

-- clowns to the left, jokers to the right (program)
def trueToLeftFalseToRight [Functional program]:
  program (a × Bool) (Thunk a ⊕ Thunk a) := function trueToLeftFalseToRightF

-- programs can perform conditional logic
def if_
  [Functional program]
  [Sequential program]
  [Creational program]
  [Conditional program]:
    program a Bool → program a b → program a b → program a b :=
      fun (a2b la2b ra2b) =>
        let_ a2b $
          in_ $
            (trueToLeftFalseToRight >=> la2b ||| ra2b)

-- trivial library level keyword
-- introduced for esthetic reasons
def else_ {a} : a → a := id

--
-- generic, implementation related, structures
--

structure FromComputationValuedFunction
  (computation : (Type u → Type u)) (a b : Type u) : Type (u+1) where
    toComputationValuedFunction : a → computation b

--
-- generic
-- Functional, Functorial, Creational, Sequential, Conditional
-- implementations
--

instance [Applicative computation]:
  Functional (FromComputationValuedFunction computation) where
    function := fun a2b => ⟨fun a => pure $ a2b a⟩

instance [Functor computation]:
  Functorial (FromComputationValuedFunction computation) where
    andThenF := fun ⟨a2cb⟩ b2c =>
      ⟨fun a => b2c <$> a2cb a⟩

instance [Applicative computation]:
  Creational (FromComputationValuedFunction computation) where
    product := fun ⟨a2cb⟩ ⟨a2cc ⟩ =>
      ⟨fun a => pure Prod.mk <*> a2cb a <*> a2cc a⟩

instance [Monad computation]:
  Sequential (FromComputationValuedFunction computation) where
    andThen := fun ⟨a2cb⟩ ⟨b2cc⟩ =>
        ⟨fun a => a2cb a >>= b2cc⟩

instance:
  Conditional (FromComputationValuedFunction computation) where
    sum := fun ⟨c2ca⟩ ⟨b2ca⟩ =>
        ⟨foldSum c2ca b2ca⟩

--
-- specific
-- Functor, Applicative, Monad
-- implementations
--

-- trivial Active implementation
structure Active (a : Type u) : Type u where
  runActive : a
deriving Repr

instance: Functor Active where

  map : {a b : Type} → (a → b) → Active a → Active b :=
    fun a2b ⟨a⟩ => ⟨a2b a⟩

instance: Applicative Active where

  pure : {a : Type} → a → Active a :=
    fun a => ⟨a⟩

  seq : {a b : Type} → Active (a → b) → (Unit → Active a) → Active b :=
    fun ⟨a2b⟩ u2aa => ⟨a2b ( (u2aa ()).runActive )⟩

 instance: Monad Active where

  bind : {a b : Type} → Active a → (a → Active b) → Active b :=
    fun ⟨a⟩ a2ab => ⟨(a2ab a).runActive⟩

--
-- specific implementation based materializations
--

-- just to get started: trivial Active materialization
def materializeActive:
  FromComputationValuedFunction Active a b → (a → b) :=
    fun ⟨a2ab⟩ => fun a => (a2ab a).runActive

--
-- primitive programs
--
-- they are program specifications, but,
-- by abuse of notation, let's call them programs
--

def isZeroF: Nat → Bool := fun a => a == 0

def isZero [Functional program]: program Nat Bool :=
  function isZeroF

def isOneF: Nat → Bool := fun a => a == 1

def isOne [Functional program]: program Nat Bool :=
  function isOneF

def oneF: Nat → Nat := fun _ => 1

def one[Functional program]: program Nat Nat := function oneF

def minusOneF: Nat → Nat := fun a => a - 1

def minusOne[Functional program]: program Nat Nat :=
  function minusOneF

def minusTwoF: Nat → Nat := fun a => a - 2

def minusTwo[Functional program]: program Nat Nat :=
  function minusTwoF

def addF: Nat × Nat → Nat :=
  fun ⟨a,b⟩ => a + b

def add [Functional program]: program (Nat × Nat) Nat :=
  function addF

def multiplyF: Nat × Nat → Nat :=
  fun ⟨a,b⟩ => a * b

def multiply [Functional program]: program (Nat × Nat) Nat :=
  function multiplyF

--
-- composite (recursive) programs
--
-- they are program specifications, but,
-- by abuse of notation, let's call them programs
--
-- 'unsafe' keyword is used because Lean (strangely enough)
-- checks termination of (abstract) program specifications instead
-- of only checking (concrete) program implementation based materializations
--

unsafe def fibonacci
  [Functional program]
  [Creational program]
  [Sequential program]
  [Conditional program]:
    program Nat Nat :=
      if_ isZero one $
        else_ $
          if_ isOne one $
            else_ $
             (minusOne >=> fibonacci) &&& (minusTwo >=> fibonacci) >=> add


unsafe def factorial
  [Functional program]
  [Creational program]
  [Sequential program]
  [Conditional program]:
    program Nat Nat :=
      if_ isZero one $
        else_ $
          let_ (minusOne >=> factorial) $
            in_ $
              multiply

--
-- let's evaluate
--

#eval (materializeActive fibonacci) 10

#eval (materializeActive factorial) 10

-- $ lean PSBP.lean
-- 89
-- 3628800

[Robin Arnez]

Luc Duponcheel schrieb:

seq : {α β : Type u} → f (α → β) → (Unit → f α) → f β
the (Unit → f α) does not really emulate lazy evaluation (evaluate zero times or one time), but rather "by name evaluation" (evaluate zero or more times). So I think that
seq : {α β : Type u} → f (α → β) → Thunk (f α) → f β
would be more efficient.

Using Thunk is unnecessary, for several reasons:

1. The caller can ensure themselves that the functions only needs to evaluate once, in the sense of:

let x : Thunk (Option Nat) := ... -- computation that we *really* don't want to run twice
f <*> x.get -- i.e. seq f (fun _ => x.get)

2. Usually, the implementation of seq already ensures that the function is only evaluated once
3. If not, the implementation can do:

instance : Applicative FunnyThing where
  seq x f :=
    let thunk := Thunk.mk f
    -- use thunk.get later

4. The definition of seq will usually be inlined and the compiler has better support for functions than for Thunks

[Robin Arnez]

(deleted)

[Robin Arnez]

Here's also a cleaned up version

Code listing

/-!
generic, specification related, functions
-/

def foldSum (c2a : c → a) (b2a : b → a) (sum : c ⊕ b) : a :=
  match sum with
  | .inl tc => c2a tc
  | .inr tb => b2a tb


-- clowns to the left, jokers to the right (function)
def trueToLeftFalseToRightF : a × Bool → a ⊕ a
  | ⟨a, true⟩ => .inl a
  | ⟨a, false⟩ => .inr a

/-!
specifications
-/

/-- functions are programs -/
class Functional (program : Type u → Type u → Type v) where
  function {a b : Type u} : (a → b) → program a b

export Functional (function)

/-- the identity function is a program -/
def identity [Functional program] : program a a :=
  function id

/-- functions can act upon programs -/
class Functorial (program : Type u → Type u → Type v) where
  andThenF {a b c : Type u} : program a b → (b → c) → program a c

/-- programs can create product values -/
class Creational (program : Type u → Type u → Type v) where
  product {a b c : Type u} :
    program a b → program a c → program a (b × c)

/--
trivial library level keyword
introduced for esthetic reasons
-/
def in_ : a → a := id

export Creational (product)

infixl:60 " &&& " => product

/-- programs can act upon themselves (i.e. programs be (sequentially) composed) -/
class Sequential (program : Type u → Type u → Type v) where
  andThen {a b c : Type u} : program a b → program b c → program a c

export Sequential (andThen)

infixl:50 " >=> " => andThen

/-- programs can create intermediate values -/
def let_
    [Functional program] [Sequential program] [Creational program] :
    program a b → (program (a × b) c → program a c) :=
  fun a2b ab2c => identity &&& a2b >=> ab2c

/-- programs can consume sum values -/
class Conditional (program : Type u → Type u → Type v) where
  sum {a b c : Type u} : program c a → program b a → program (c ⊕ b) a

export Conditional (sum)

infixl:55 " ||| " => sum

/-- clowns to the left, jokers to the right (program) -/
def trueToLeftFalseToRight [Functional program] :
  program (a × Bool) (a ⊕ a) := function trueToLeftFalseToRightF

/-- programs can perform conditional logic -/
def if_
    [Functional program]
    [Sequential program]
    [Creational program]
    [Conditional program] :
    program a Bool → program a b → program a b → program a b :=
  fun a2b la2b ra2b =>
    let_ a2b $
      in_ $
        (trueToLeftFalseToRight >=> la2b ||| ra2b)

/--
trivial library level keyword
introduced for esthetic reasons
-/
def else_ {a} : a → a := id

/-!
generic, implementation related, structures
-/

structure FromComputationValuedFunction
    (computation : (Type u → Type u)) (a b : Type u) where
  toComputationValuedFunction : a → computation b

/-!
generic
Functional, Functorial, Creational, Sequential, Conditional
implementations
-/

instance [Applicative computation] :
    Functional (FromComputationValuedFunction computation) where
  function := fun a2b => ⟨fun a => pure $ a2b a⟩

instance [Functor computation] :
    Functorial (FromComputationValuedFunction computation) where
  andThenF := fun ⟨a2cb⟩ b2c => ⟨fun a => b2c <$> a2cb a⟩

instance [Applicative computation] :
    Creational (FromComputationValuedFunction computation) where
  product := fun ⟨a2cb⟩ ⟨a2cc⟩ =>
    ⟨fun a => pure Prod.mk <*> a2cb a <*> a2cc a⟩

instance [Monad computation] :
    Sequential (FromComputationValuedFunction computation) where
  andThen := fun ⟨a2cb⟩ ⟨b2cc⟩ => ⟨fun a => a2cb a >>= b2cc⟩

instance : Conditional (FromComputationValuedFunction computation) where
  sum := fun ⟨c2ca⟩ ⟨b2ca⟩ => ⟨foldSum c2ca b2ca⟩

/-!
specific
Functor, Applicative, Monad
implementations
-/

abbrev Active := Id

/-!
specific implementation based materializations
-/

-- just to get started: trivial Active materialization
def materializeActive : FromComputationValuedFunction Active a b → (a → b) :=
  fun ⟨a2ab⟩ => fun a => (a2ab a).run

/-!
primitive programs

they are program specifications, but,
by abuse of notation, let's call them programs
-/

def isZeroF: Nat → Bool := fun a => a == 0

def isZero [Functional program] : program Nat Bool :=
  function isZeroF

def isOneF : Nat → Bool := fun a => a == 1

def isOne [Functional program] : program Nat Bool :=
  function isOneF

def oneF : Nat → Nat := fun _ => 1

def one [Functional program] : program Nat Nat := function oneF

def minusOneF : Nat → Nat := fun a => a - 1

def minusOne [Functional program] : program Nat Nat :=
  function minusOneF

def minusTwoF : Nat → Nat := fun a => a - 2

def minusTwo [Functional program] : program Nat Nat :=
  function minusTwoF

def addF : Nat × Nat → Nat :=
  fun ⟨a,b⟩ => a + b

def add [Functional program] : program (Nat × Nat) Nat :=
  function addF

def multiplyF : Nat × Nat → Nat :=
  fun ⟨a, b⟩ => a * b

def multiply [Functional program] : program (Nat × Nat) Nat :=
  function multiplyF

/-
composite (recursive) programs

'unsafe' keyword is used because Lean (strangely enough)
checks termination of (abstract) program specifications instead
of only checking (concrete) program implementation based materializations
-/

unsafe def fibonacci
    [Functional program]
    [Creational program]
    [Sequential program]
    [Conditional program] :
    program Nat Nat :=
  if_ isZero one $
    else_ $
      if_ isOne one $
        else_ $
          (minusOne >=> fibonacci) &&& (minusTwo >=> fibonacci) >=> add


unsafe def factorial
    [Functional program]
    [Creational program]
    [Sequential program]
    [Conditional program] :
    program Nat Nat :=
  if_ isZero one $
    else_ $
      let_ (minusOne >=> factorial) $
        in_ $
          multiply

/-!
let's evaluate
-/

#eval (materializeActive fibonacci) 10

#eval (materializeActive factorial) 10

-- $ lean PSBP.lean
-- 89
-- 3628800

I've adjusted the formatting and indentation, removed Thunk for the sum type (I think it's unnecessary..?) and replaced Active with Id which already exists in the core library.

[Luc Duponcheel]

Robin Arnez, just back from a cycling trip (I am also an addicted (race bicycle) cyclist and (green house) gardener), thanks so much for your constructive comments. What a positive community, this Lean community! In fact, with the standard Sum type the Thunk's are indeed not necessary. Gonna update my code.

[Luc Duponcheel]

Robin Arnez, by the way, which formatter do you use? Is it a command-line one? Can it be integrated with vscode?

[Luc Duponcheel]

Shreyas Srinivas, I was thinking (.. .while cycling on my race bicycle ...).
There are two things: programming and proving properties .
I want to do both.
But do I really want to prove properties of (potentially unsafe) programs?
Maybe not.
I want to prove properties of the type class members (such as associativity of program sequential composition using computation (monad) laws).

So, I am going to continue "living unsafe (in a disciplined way) and hoping for the best" and learn how to prove laws such as the associativity one mentioned above.

[Shreyas Srinivas]

You probably want to look at docs#LawfulMonad and docs#LawfulApplicative then. By imposing this typeclass constraint on your monad, you get the monad laws for free

[Shreyas Srinivas]

The distinction is made because it might be tedious to always prove that actual monads behave lawfully. For example the IO monad.

[Shreyas Srinivas]

Also you might want to check out the new (in beta essentially) monadic verification framework that attaches a program logic into monads. #general > new monadic program verification framework

[Luc Duponcheel]

Shreyas Srinivas, thanks for your tip. I have looked at those docs already, but, frankly, I am starting to learn about all those fantastic Lean proving capabilities. Stay in touch, please.

[Robin Arnez]

Luc Duponcheel schrieb:

I can imagine that those fixed points are akin to catamorphisms (I used them in the 90-ties when I worked in Utrecht with the group of Erik Meijer) but somewhat modified to yield an Option result in order to transform a partial function into a global one, right?

I'm not sure about catamorphisms but the idea is the following: Lean is primarily a math language and as such objects behave like "math objects" so in particular there is no such thing as a "natural number that doesn't terminate". As such, a general purpose fixpoint can be proven incorrect because it would imply something like

def abc : Nat := abc + 1

could exist. However, this would imply abc = abc + 1 which is mathematically unsound. So there are several strategies to still allow for recursion:

1. Recursion "by termination": If a function terminates, there isn't any "doesn't terminate" problem and everything works fine. Lean implements this as well-founded recursion which requires you to prove that your parameters "decrease" by some well-founded notion of less-than.
2. Partial recursion: Compiles the recursion as normal but hides the body of the declaration for proofs. That means that you can write functions that recurse indefinitely but can't prove anything about them.
3. Recursion by monotonicity (partial_fixpoint): This one uses a fact from order theory that in certain orders, all monotone functions have a fixpoint. Here you can work with an Option type that means something like: none if it doesn't terminate and some x if it does terminate and returns x. In the kind of orders you're going to work with, x <= y means something like "if it terminated for some input in x, it will terminate with the same result in y". Then, in order to get the fixpoint of a function f, you need to prove monotonicity of f which amounts to proving that if from x to y nothing changed that terminated before, then in the result, from f x to f y also nothing changed that terminated before.

[Luc Duponcheel]

Robin Arnez, thanks again for your information.
Catamorphism is +/- just a fancy word for structural recursion, and corresponds more or less to what you explained in 3. , see Catamorphism.

By that way, wiki page mentions the original https://maartenfokkinga.github.io/utwente/mmf91m.pdf paper (Erik Meijer is one of the authors). The paper was written a year before I joined the team for a short time.

Anway, I am first going to concentrate on programming and only proving laws of my type classes, e.g. associativity, in terms of the Functor, Applicative and Monad laws (in other words, not on any laws of programs written using my library level programming language (using the members of my type classes)).

I am also going to start a GitHub project.

I guess that if you wrote "math object" you meant "constructive math object". Using the "axiom of choice" (infinite product of non-empty sets is non-empty) there exist math objects that cannot be constructed.

[Luc Duponcheel]

Robin Arnez, by the way, which code formatter do you use? Is there a command-line one? Is there one that can be integrated with vscode? Sorry for repeating the question.

[Patrick Massot]

There is no automatic code formatter for Lean. This has been discussed many times, you can search on this Zulip. The short story is that the syntax extensibility of Lean makes it a lot harder than for regular programming languages. It will come at some point, but this is a lot more work than you would think.

[Luc Duponcheel]

Patrick Massot, frankly I am the kind of person who admires the
people building projects like Lean rather than underestimating their work :+1: .

[Patrick Massot]

I’m sorry, my message was probably unclear. My intend was not at all to complain about anything you wrote. Asking for a code formatter is a very natural thing to do those days. We very much understand why people can expect this. I simply tried to explain why it’s not there yet.

[Patrick Massot]

And I apologize if you felt I was accusing you of underestimating the work of people building Lean and its tooling.

[Arthur Paulino]

I'm particularly excited for the big shake up diffs on Lean 4 repos when the formatter come out :eyes:

[Luc Duponcheel]

Folks, I just created a new (preliminary) GitHub project,

https://github.com/LucDuponcheelAtGitHub/LeanPSBP.

Those who are inclined may also be interested in
https://github.com/LucDuponcheelAtGitHub/yoneda (code is Scala, docs are LaTeX)

and those who are interested in "understanding a universe framework by programming it" may also be interested in
https://github.com/LucDuponcheelAtGitHub/timeHybrids.

The "Time Hybrids" book, by Fred Van Oystaeyen, explains an algebraic geometry instead of analytic geometry based approach to the "universe". Fred has an, i.m.h.o. , highly underestimated mathematician's vision on reality.

... sorry for doing free advertising ...

[Luc Duponcheel]

Hello, I am trying to document my code in a similar way as the FPIL and TPIL documentation. So I downloaded the FPIL GitHub source, and, as a experiment, tried to add an extra section on PSBP. So far so good, but I encountered a strange error with anchors. So far I defined three anchors, Functional, Identity and Functorial in Examples, and used them in FPLean. Strangely enough everything worked out fine for the first two anchors but for the third one I get the following error

Code listing

$ lake exe fp-lean
⚠ [144/399] Replayed VersoManual.InlineLean
warning: src/verso-manual/VersoManual/InlineLean.lean:646:8: unused variable `col?`

Note: This linter can be disabled with `set_option linter.unusedVariables false`
ℹ [151/399] Replayed book/buildExamples
info: Building examples in ../examples
✖ [391/399] Building FPLean.ProgramSpecifications.Class
trace: .> LEAN_PATH=/home/luc/GitHub/Lean/fp-lean-master/book/.lake/packages/subverso/.lake/build/lib/lean:/home/luc/GitHub/Lean/fp-lean-master/book/.lake/packages/MD4Lean/.lake/build/lib/lean:/home/luc/GitHub/Lean/fp-lean-master/book/.lake/packages/verso/.lake/build/lib/lean:/home/luc/GitHub/Lean/fp-lean-master/book/.lake/build/lib/lean /home/luc/.elan/toolchains/leanprover--lean4---v4.22.0-rc4/bin/lean /home/luc/GitHub/Lean/fp-lean-master/book/FPLean/ProgramSpecifications/Class.lean -o /home/luc/GitHub/Lean/fp-lean-master/book/.lake/build/lib/lean/FPLean/ProgramSpecifications/Class.olean -i /home/luc/GitHub/Lean/fp-lean-master/book/.lake/build/lib/lean/FPLean/ProgramSpecifications/Class.ilean -c /home/luc/GitHub/Lean/fp-lean-master/book/.lake/build/ir/FPLean/ProgramSpecifications/Class.c --setup /home/luc/GitHub/Lean/fp-lean-master/book/.lake/build/ir/FPLean/ProgramSpecifications/Class.setup.json --json
error: FPLean/ProgramSpecifications/Class.lean:47:77: Anchor not found.



Hint: Use a defined anchor
  • F̵u̵n̵c̵t̵o̵r̵i̵a̵l̵F̲u̲n̲c̲t̲i̲o̲n̲a̲l̲
  • F̵u̵n̵c̵t̵o̵r̵i̵a̵l̵I̲d̲e̲n̲t̲i̲t̲y̲
error: FPLean/ProgramSpecifications/Class.lean:50:10: Anchor not found.



Hint: Use a defined anchor
  • F̵u̵n̵c̵t̵o̵r̵i̵a̵l̵F̲u̲n̲c̲t̲i̲o̲n̲a̲l̲
  • F̵u̵n̵c̵t̵o̵r̵i̵a̵l̵I̲d̲e̲n̲t̲i̲t̲y̲
error: Lean exited with code 1
Some required builds logged failures:
- FPLean.ProgramSpecifications.Class
error: build failed

The documentation fragments are

Code listing

import ExampleSupport

set_option linter.unusedVariables false

namespace Class

variable {α β γ: Type}
-- ANCHOR: Functional
class Functional (program : Type u → Type u → Type v) where
  asProgram {α β : Type u} : (α → β) → program α β
-- ANCHOR_END: Functional

export Functional (asProgram)

-- ANCHOR: Identity
def identity [Functional program] : program α α :=
  asProgram id
-- ANCHOR_END: Identity

-- ANCHOR: Functorial
class Functorial (program : Type u → Type u → Type v) where
  andThenF {α β γ : Type u} : program α β → (β → γ) → program α γ
-- ANCHOR_END: Functorial

export Functorial (andThenF)

end Class

and

Code listing

import VersoManual
import FPLean.Examples

open Verso.Genre Manual
open Verso Code External

open FPLean

set_option verso.exampleProject "../examples"
set_option verso.exampleModule "Examples.ProgramSpecifications.Class"

#doc (Manual) "The Program Specification Type Classes" =>

So far we have seen type classes {lit}`Functor`, {lit}`Applicative` and {lit}`Monad` that are computation
specifications. Think of computations as effectful expressions. They are operational artifacts. They do not really have
a meaning in the mathematical sense. Functions, on the other hand, are denotational artifacts. They do have a meaning in
the mathematical sense. So what are effectful function specifications? That is what we are going to see in this section.

# {lit}`class Functional`

Functions can, somehow, be used as programs. Well, that's what functional programming is all about. Functions that are
used as programs are effectless. We can define functions as programs in a formal way by defining a type class. This is
what we do with the {anchorName Functional}`Functional` class.

:::paragraph
```anchor Functional
class Functional (program : Type u → Type u → Type v) where
  asProgram {α β : Type u} : (α → β) → program α β

:::

{lit}def identity

Below is a simple, standard, but extremely useful example of a function as a program,
the {anchorName Identity}identity program.

:::paragraph

def identity [Functional program] : program α α :=
  asProgram id

:::

{lit}class Functorial

Functions can act upon programs. They do that in an effecless way. We can define functions acting upon programs in a
formal way by defining a type class. This is what we do with the {anchorName Functorial}Functorial class.

:::paragraph

class Functorial (program : Type u → Type u → Type v) where
  andThenF {α β γ : Type u} : program α β → (β → γ) → program α γ

:::

````

[Luc Duponcheel]

sorry folks the triple backquotes in my code are sitting in the way of properly showing the last code (any hints?)

[Shreyas Srinivas]

Verso is fairly new and doesn't have too many references to learn from. I'd recommend checking with @David Thrane Christiansen (CC)

[Luc Duponcheel]

Shreyas Srinivas, will do!

[Luc Duponcheel]

Hello, what a fantastic community, @David Thrane Christiansen helped me out !!!

[Luc Duponcheel]

Hello folks,

I pushed a first (preliminary) version of the documentation of the PSBP library to psbpDocumentation.

As usual you can make a local multi-html version (see README.md).

I also updated the PSBP library itself to use more Greek letters.

All comments are welcome

[Luc Duponcheel]

Hello,

First some context

My PSBP library can be seen as a library level pointfree programming language.
So I have, for example, defined library level keywords let_, in_, if_ and else_.
PSBP can also (and sometimes has to) be used as a positional programming language,
accessing values on a runtime stack by position. Especially for sequential
"recipe-like" scripts, accessing products of the initial and/or intermediate values
on the runtime stack. That being said ...

Here is my technical question

I am translating my Haskell code to Lean, more precisely my code for yet another
library level keyword at_ to access products of the initial and/or intermediate values
on the runtime stack. The code of at_ is below (lines 76 to 88).
You can also search for at_.
The intention is to also define a convenient operation symbol, but that's another matter.

Code listing

class Functional (program : Type u → Type u → Type v) where
  asProgram {α β : Type u} :
    (α → β) → program α β

export Functional (asProgram)

class Functorial (program : Type u → Type u → Type v) where
  andThenF {α β γ : Type u} :
    program α β → (β → γ) → program α γ

export Functorial (andThenF)

infixl:50 " >-> " => andThenF

class Creational (program : Type u → Type u → Type v) where
  product {α β γ : Type u} :
    program α β → program α γ → program α (β × γ)

export Creational (product)

infixl:60 " &&& " => product

class Sequential (program : Type u → Type u → Type v) where
  andThen {α β γ : Type u} :
    program α β → program β γ → program α γ

export Sequential (andThen)

infixl:50 " >=> " => andThen

class Conditional (program : Type u → Type u → Type v) where
  sum {α β γ : Type u} :
    program γ α → program β α → program (γ ⊕ β) α

export Conditional (sum)

infixl:55 " ||| " => sum

def identity [Functional program] :
    program α α :=
  asProgram id

def let_
    [Functional program]
    [Sequential program]
    [Creational program] :
    program α β → (program (α × β) γ → program α γ) :=
  λ αpβ αaβpγ => identity &&& αpβ >=> αaβpγ

def in_ : α → α := id

def trueToLeftFalseToRightF : α × Bool → α ⊕ α
  | ⟨α, true⟩ => .inl α
  | ⟨α, false⟩ => .inr α

def trueToLeftFalseToRight [Functional program] :
  program (α × Bool) (α ⊕ α) :=
    asProgram trueToLeftFalseToRightF

def if_
    [Functional program]
    [Sequential program]
    [Creational program]
    [Conditional program] :
    program α Bool →
    program α β →
    program α β →
    program α β :=
  λ αpb t_apβ f_apβ =>
    let_ αpb $
      in_ $
        trueToLeftFalseToRight >=> t_apβ ||| f_apβ

def else_ : α → α := id

def at_
    [Functional program]
    [Creational program]
    [Sequential program] :
    program α β →
    program σ α →
    program (σ × β) γ →
    program σ γ :=
  -- λ αpβ σpα =>
  --   let σpβ : program σ β := σpα >=> αpβ
  --   let_ σpβ
  λ αpβ σpα =>
    let_ σpα >=> αpβ

--------------------------------------------------------------------------------

def andThenF'
    [Functional program]
    [Sequential program] :
    program α β → (β → γ) → program α γ :=
  λ αpβ => λ βfγ => αpβ >=> asProgram βfγ

instance [Functional program] [Sequential program] :
    Functorial program where
  andThenF := andThenF'

--------------------------------------------------------------------------------

structure FromComputationValuedFunction
    (computation : (Type u → Type u)) (α β : Type u) where
  toComputationValuedFunction : α → computation β

instance [Applicative computation] :
    Functional
    (FromComputationValuedFunction computation) where
  asProgram := λ αfβ => ⟨λ α => pure $ αfβ α⟩


instance [Functor computation] :
    Functorial
    (FromComputationValuedFunction computation) where
  andThenF := λ ⟨αfcβ⟩ => λ βfγ => ⟨λ α => βfγ <$> αfcβ α⟩

instance [Applicative computation] :
    Creational (FromComputationValuedFunction computation) where
  product := λ ⟨αfcβ⟩ ⟨αfcγ⟩ =>
    ⟨λ α => pure Prod.mk <*> αfcβ α <*> αfcγ α⟩

instance [Monad computation] :
    Sequential
    (FromComputationValuedFunction computation) where
  andThen := λ ⟨αfcβ⟩ ⟨βfcγ⟩ => ⟨λ α => αfcβ α >>= βfcγ⟩

def foldSum
    (γfα : γ → α)
    (βfα : β → α)
    (sum : γ ⊕ β) : α :=
  match sum with
  | .inl tc => γfα tc
  | .inr tb => βfα tb

instance :
    Conditional
    (FromComputationValuedFunction computation) where
  sum := λ ⟨γfγα⟩ ⟨βfγα⟩ => ⟨foldSum γfγα βfγα⟩

--------------------------------------------------------------------------------

Similar (almost identical) Haskell code compiles fine.
You can run it the usual way using the little icon on
the top right corner of the code block to open it in
the lean scratch pad online.

Code listing

overloaded, errors
  type mismatch
    ?m.9772 >=> αpβ
  has type
    program ?m.9687 β : Type ?u.9619
  but is expected to have type
    program (σ × β) γ → program σ γ : Type ?u.9619

  88:9 Application type mismatch: In the application
    let_ σpα
  the argument
    σpα
  has type
    program σ α : Type ?u.9619
  but is expected to have type
    program σ β : Type ?u.9619

[Aaron Liu]

You want

  λ αpβ σpα =>
    let_ (σpα >=> αpβ)

[Aaron Liu]

functions bind their arguments very very tightly

[Luc Duponcheel]

Aaron, sorry copy/paste error (btw, see code above it with a normal language level let).
With your suggestion (and the code above) I still have an error

Code listing

stuck at solving universe constraint
  max ?u.9684 ?u.9685 =?= max ?u.9652 ?u.9653
while trying to unify
  program (Prod.{max ?u.9653 ?u.9652, max ?u.9653 ?u.9652} σ β) γ → program σ γ : Type ?u.9619
with
  program (Prod.{max ?u.9685 ?u.9684, max ?u.9685 ?u.9684} σ β) γ → program σ γ : Type ?u.9619

even more confusing for me, here is the corrected code

Code listing

class Functional (program : Type u → Type u → Type v) where
  asProgram {α β : Type u} :
    (α → β) → program α β

export Functional (asProgram)

class Functorial (program : Type u → Type u → Type v) where
  andThenF {α β γ : Type u} :
    program α β → (β → γ) → program α γ

export Functorial (andThenF)

infixl:50 " >-> " => andThenF

class Creational (program : Type u → Type u → Type v) where
  product {α β γ : Type u} :
    program α β → program α γ → program α (β × γ)

export Creational (product)

infixl:60 " &&& " => product

class Sequential (program : Type u → Type u → Type v) where
  andThen {α β γ : Type u} :
    program α β → program β γ → program α γ

export Sequential (andThen)

infixl:50 " >=> " => andThen

class Conditional (program : Type u → Type u → Type v) where
  sum {α β γ : Type u} :
    program γ α → program β α → program (γ ⊕ β) α

export Conditional (sum)

infixl:55 " ||| " => sum

def identity [Functional program] :
    program α α :=
  asProgram id

def let_
    [Functional program]
    [Sequential program]
    [Creational program] :
    program α β → (program (α × β) γ → program α γ) :=
  λ αpβ αaβpγ => identity &&& αpβ >=> αaβpγ

def in_ : α → α := id

def trueToLeftFalseToRightF : α × Bool → α ⊕ α
  | ⟨α, true⟩ => .inl α
  | ⟨α, false⟩ => .inr α

def trueToLeftFalseToRight [Functional program] :
  program (α × Bool) (α ⊕ α) :=
    asProgram trueToLeftFalseToRightF

def if_
    [Functional program]
    [Sequential program]
    [Creational program]
    [Conditional program] :
    program α Bool →
    program α β →
    program α β →
    program α β :=
  λ αpb t_apβ f_apβ =>
    let_ αpb $
      in_ $
        trueToLeftFalseToRight >=> t_apβ ||| f_apβ

def else_ : α → α := id

def at_
    [Functional program]
    [Creational program]
    [Sequential program] :
    program α β →
    program σ α →
    program (σ × β) γ →
    program σ γ :=
  -- λ αpβ σpα =>
  --   let σpβ : program σ β := σpα >=> αpβ
  --   let_ σpβ
  λ αpβ σpα =>
    let_ (σpα >=> αpβ)

--------------------------------------------------------------------------------

def andThenF'
    [Functional program]
    [Sequential program] :
    program α β → (β → γ) → program α γ :=
  λ αpβ => λ βfγ => αpβ >=> asProgram βfγ

instance [Functional program] [Sequential program] :
    Functorial program where
  andThenF := andThenF'

--------------------------------------------------------------------------------

structure FromComputationValuedFunction
    (computation : (Type u → Type u)) (α β : Type u) where
  toComputationValuedFunction : α → computation β

instance [Applicative computation] :
    Functional
    (FromComputationValuedFunction computation) where
  asProgram := λ αfβ => ⟨λ α => pure $ αfβ α⟩


instance [Functor computation] :
    Functorial
    (FromComputationValuedFunction computation) where
  andThenF := λ ⟨αfcβ⟩ => λ βfγ => ⟨λ α => βfγ <$> αfcβ α⟩

instance [Applicative computation] :
    Creational (FromComputationValuedFunction computation) where
  product := λ ⟨αfcβ⟩ ⟨αfcγ⟩ =>
    ⟨λ α => pure Prod.mk <*> αfcβ α <*> αfcγ α⟩

instance [Monad computation] :
    Sequential
    (FromComputationValuedFunction computation) where
  andThen := λ ⟨αfcβ⟩ ⟨βfcγ⟩ => ⟨λ α => αfcβ α >>= βfcγ⟩

def foldSum
    (γfα : γ → α)
    (βfα : β → α)
    (sum : γ ⊕ β) : α :=
  match sum with
  | .inl tc => γfα tc
  | .inr tb => βfα tb

instance :
    Conditional
    (FromComputationValuedFunction computation) where
  sum := λ ⟨γfγα⟩ ⟨βfγα⟩ => ⟨foldSum γfγα βfγα⟩

--------------------------------------------------------------------------------

[Aaron Liu]

that means you need to be more explicit with your universes

[Luc Duponcheel]

Ok, I'll give it a try, all suggestions are welcome.

[Patrick Massot]

The suggestion is to replace all those Type u and Type v with Type and forget about universes.

[Patrick Massot]

I’m pretty sure you Haskell code doesn’t have universes.

[Patrick Massot]

And note most of Lean 4 programming infrastructure is Type only.

[Patrick Massot]

You can help Lean by putting variable {program : Type u → Type u → Type v} {α β γ σ : Type u} around line 38.

[Patrick Massot]

But you will immediately see that your if_ is already not doing what you want.

[Patrick Massot]

Since Bool only lives in Type and you want program : Type u → Type u → Type v.

[Luc Duponcheel]

It does not have universes indeed. I copy/pated from Monad and friends where there is also a : Type (max (u+1) v) which I already tried. and I also tried

Code listing

def at_{program : Type u → Type u → Type v} {σ α β γ : Type u}
    [Functional program]
    [Creational program]
    [Sequential program] :
    program α β →
    program σ α →
    program (σ × β) γ →
    program σ γ :=
  -- λ αpβ σpα =>
  --   let σpβ : program σ β := σpα >=> αpβ
  --   let_ σpβ
  λ αpβ σpα =>
    let_ (σpα >=> αpβ)

did not work.

I'll try with variable ...

[Luc Duponcheel]

Should I also somewhere use something similar to : Type (max (u+1) v) in my def of at_? I do not know the syntax for def's (I know the syntax for classes, cfr. Monad and friends) ... . My aim is to also state and prove laws, so I guess that the universes will eventually be necessary anyway (or not?)
.

[Luc Duponcheel]

btw, the α stands for "stack", and σ × β means β pushed onto σ.

[Luc Duponcheel]

Patrick, your suggestion to only use Type did the trick. But are you sure I'll never need the Type u and Type v like done in the Prelude.lean with Monad and friends (I mean, when doing theorem proving of my laws in terms of the laws of Monad and friends)?

[Patrick Massot]

All the monads that are used when programming in Lean are Type only.

[Patrick Massot]

It starts with docs#IO

[Luc Duponcheel]

Patrick, fair enough, but why then all those universes in Prelude.lean?
btw, what precisely starts at docs#IO?

Code listing

class Monad (m : Type u → Type v) : Type (max (u+1) v) extends Applicative m, Bind m where
  map      f x := bind x (Function.comp pure f)
  seq      f x := bind f fun y => Functor.map y (x ())
  seqLeft  x y := bind x fun a => bind (y ()) (fun _ => pure a)
  seqRight x y := bind x fun _ => y ()

[Patrick Massot]

Monads also play a role in maths, not only programming. I guess this is why they have universes. What I had in mind with IO all the monads that are used in meta-programming in Lean. They are all built on top of IO using monad transformers.

[Patrick Massot]

Anyway, maybe I wrote too much. My recommendation is to at least start without all those universes. There is enough to do without worrying about universes.

[Luc Duponcheel]

Thanks so much for your suggestion.
Just like with my documentation, I'll start "lazily" simple and, maybe, later, add complexity by need. About IO... When programming PSBP in Haskell I used MonadIO a lot in order to use my "library level" programs together with IO. Especially for the logging of my parallel operator, used in a parallel version of fibonacci(implemented using hakka, an Actor library for Haskell). I would like to implement something like hakka in Lean as well.

But there are ony 24 hours in a day :grinning: .

[Luc Duponcheel]

Folks,

Thanks for all constructive replies.

I could get rid of the error, even without giving up the

{σ α β γ : Type u}
and
(program : Type u → Type u → Type v) : Type (max (u+1) v)

"universe mumbo-jumbo" by defining
a class Positional
and
an instance ... Positional where ...

It is all a bit "trial and error" for me, but, from a semantic point
of view, this class + instance approach actually makes sense.

I hope now that my examples will work as well

Code listing

class Positional (program : Type u → Type u → Type v) : Type (max (u+1) v) where
  at_ {σ α β γ : Type u} :
      program α β →
      program σ α →
      program (σ × β) γ →
      program σ γ

infixl:45 " @@@ " => at_

instance
    [Functional program]
    [Creational program]
    [Sequential program] :
    Positional program where
    at_ {σ α β γ : Type} :
      program α β →
      program σ α →
      program (σ × β) γ →
      program σ γ :=
        λ αpβ σpα =>
          let_ (σpα >=> αpβ)

[Luc Duponcheel]

Folks,

I added positional programming and stateful programming and updated the documentation. The documentation will, eventually, become a "github.io"
web page, but I am still struggling a with how to configure everything.

see
https://github.com/LucDuponcheelAtGitHub/PSBP
and
https://github.com/LucDuponcheelAtGitHub/psbpDocumentation

For now, for the documentation, you'll have to

• download the .zip file and unzip it,
• [optionally] run "$ lake exe psbpDocumentation --output _out/html --depth 2"
• look at the documentation locally as "htm-multi" of "html-single".
  For example, on my laptop,
  file:///home/luc/GitHub/Lean/psbpDocumentation/_out/html/html-multi/index.html
  I am truly sorry.

Of course everything is preliminary work, but all comments are welcome.

[Luc Duponcheel]

I added programming with failure and it's documentation.

The situation now is

1. Warning
2. Introduction
3. The PSBP Library type classes
4. fibonacci and factorial
5. What about Functorial?
6. Computation Valued Functions
7. ActiveProgram
8. ReactiveProgram
9. Positional Programming
10. Programming With State
11. Programming With Failure

Of course everything is preliminary work, but all comments are welcome.

I hope you folks do not consider this as "spam".

[Luc Duponcheel]

Hello folks, I updated programming with failure and it's documentation and added a section on validating failure, accumulating failures (Applicative based implementation) as opposed to the already existing section on fail-fast failure, only considering first failure, (Monad based implementation).

The (slightly changed) situation is now

1. Warning
2. Introduction
3. The PSBP Library type classes
4. fibonacci and factorial
5. Computation Valued Functions
6. ActiveProgram
7. ReactiveProgram
8. Positional Programming
9. Programming With State
10. Programming With Failure

Sorry for all my posts, hopefully the set of interested people is not empty.
And, once again, all comments are welcome.

For now I am going to (temporarily) stop adding extra programming features
and concentrate on defining appropriate "program and friends" related laws, and prove "program and friends" related theorems in terms of "monad and friends" related laws.

But I am still learning the (exiting(!)) theorem proving part of Lean (the very reason for me to switch from Haskell to Lean).

Thanks for reading.

[Luc Duponcheel]

Hello, folks, I added an introduction and added laws and proofs.

The content is now

1. About
2. Naming conventions
3. Programs versus Computations
4. The PSBP library type classes
5. fibonacci and factorial
6. Laws
7. Computation Valued Functions
8. Theorems
9. ActiveProgram
10. ReactiveProgram
11. Positional Programming
12. Programming With State
13. Programming With Failure

Once again, sorry for all my posts, hopefully the set of interested people is not empty. And, once again, all comments are welcome.

[Luc Duponcheel]

Hello folks, I decided to document the PSBP library in the README.md file of the PSBP repository itself. Agreed, a bit more "low profile" than other Lean documentation. The documentation is also a kind of course with exercises and solutions.

Once again, sorry for all my posts, hopefully the set of interested people is not empty. And, once again, all comments are welcome.