Welcome to the Functional Programming Zulip Chat Archive. You can join the chat here. A common pattern I stumbled upon while implementing small logic checkers is using a list monad to do computations with backtracking then returning true or false depending on whether the list is empty (nonempty list means there is at least one solution). However, this practice doesn't make intention clear in the function type. Today, I converted this small minimal logic checker I wrote a while ago to the following:

``````module Lean where

-- http://ceur-ws.org/Vol-2271/paper1.pdf

import Data.Bifunctor

data Term
= Var Char
| Impl Term Term
deriving (Eq, Show)

prove :: Term -> Bool
prove = ljt []

ljt :: [Term] -> Term -> Bool
ljt env t
| elem t env = True
ljt env (Impl a b) = ljt (a : env) b
ljt env t = not . null \$ do
(Impl a b, env) <- select env
case a of
Var a -> do
guard \$ elem (Var a) env
guard \$ ljt (b : env) t
Impl c d -> do
guard \$ ljt (Impl d b : env) (Impl c d)
guard \$ ljt (b : env) t

select :: [a] -> [(a, [a])]
select (x:xs) = (x, xs) : map (second (x:)) (select xs)
select []     = []
``````

Any feedback on this style? Mainly the consecutive `guard \$ ...`.

A lean prover for minimal logic. GitHub Gist: instantly share code, notes, and snippets. if you want to make intent more clear in the types, wouldn't it be best to return the actual solution itself instead of a `Bool`? as proof that you found it