Nondeterministic booleans - Haskell

Welcome to the Functional Programming Zulip Chat Archive. You can join the chat here.

Pedro Minicz

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 Control.Monad
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.
Georgi Lyubenov // googleson78

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