Mně to pro čisté funkce ve smyslu https://en.wikipedia.org/wiki/Pure_function přijde v pořádku. Otázka definice nebo je i s nimi problém?
Kdyby chtěl někdo vidět kód (à la ML), tak funkce
def decBy1 : Nat -> Nat
-- Nat = {0, 1, 2, ...}
není totální, protože není definovaná pro nulu.
Totality se dá dosáhnout rozšířením návratové hodnoty na součtový typ:
def decBy1 : Nat -> Option Nat
| .succ n => .some n
| .zero => .none
Nebo zúžením def. oboru funkce:
def decBy1 (n : Nat) (_ : n≠0) : Nat :=
match n with
| .succ n => n
Memoizace pak bude fungovat pro obě funkce, v tom druhém případě se nebudou ukládat neplatné vstupy (a výsledek se nemusí vázat přes Kleisliho nesmysle).
To je narážka na to, že tomu rozumí jen 1% vývojářů (když vynecháme frontend, tak 2%). Ten zbytek svou ignoranci omlouvá tím, že to označuje za zbytečné nesmysly.
A poněkud vážněji, je nesmysl používat zbytečně složitou a abstraktní konstrukci (i když jinde se může náramně hodit, sama o sobě tedy nesmyslem není), když existuje jednodušší a čitelnější řešení, jehož podstatu každý zná ze ZŠ matematiky (i když plné pochopení toho, co se pak odehrává v rámci statické kontroly, překladu a za běhu zas tak jednoduché není, ale pořád o řád lepší než Kleisli).