Curry

Curry supports both functional programming and logic programming. It reuses Haskell syntax and type system, but extends the semantics to add logic programming.

I can’t explain logic programming now; but I can after I present the main extra features of Curry.

Laziness

Curry is lazy like Haskell:

zs = 0 : zs
thisIsOK = take 3 zs   -- gives finite list in finite time

Non-Determinism

Function (top-level or local) and top-level constants can have multiple definitions; the meaning is multiple answers.

luckyNumber = 7
luckyNumber = 8

offByOne n = n + 1
offByOne n = n - 1

offByOne luckyNumber gives 4 answers: 8, 9, 6, 7.

Simple model:

• Think of multisets of answers. (Even better: Doctor Strange in the Marvel Cinematic Multiverse of Madness. 😈)
• Function application: Apply function to every element in input multiset.
• Flatten nested multisets.
• My notation for multiset: “x; y; …” or “(x; y; …)”. I omit parentheses whenever possible to reduce clutter, given that nesting is flattened anyway (equivalently, “;” acts like associative).

Reasoning example:

  offByOne luckyNumber
= luckyNumber + 1; luckyNumber - 1
= (7; 8) + 1; (7; 8) - 1
= 7+1; 8+1; 7-1; 8-1
= 7+1; 8+1; 7-1; 8-1
= 8; 9; 6; 7

Functions and constants can be partially defined, i.e., lack definitions for some cases; the meaning is no answer for the lacking cases.

restrictEven n | mod n 2 == 0 = n
-- For odd n, no definition, so no answer.

It doesn’t say what answer to give for odd numbers, so restrictEven 7 outputs no answer. Simple model: the empty multiset. My notation: ∅. (Given flattening, ∅ acts like the identity of “;”.)

Reasoning example:

  restrictEven (offByOne luckyNumber)
= restrictEven (8; 9; 6; 7)
= restrictEven 8; restrictEven 9; restrictEven 6; restrictEven 7
= 8; ∅; 6; ∅
= 8; 6

This aspect is different from Haskell. In Haskell, restrictEven 7 is ⊥, and becomes a runtime error if evaluated. In Curry, it is not ⊥, instead the set of answers is empty, which falls under different rules.

With non-determinism, you can factor a search algorithm into: a non-deterministic definition that generates candidates, and a partial function that passes/fails candidates.

Local Constants

Local constants (let and where) are treated differently from global constants; the intention is to be easier to understand.

Local constants cannot have multiple definitions:

-- This is a compile-time error.
a = b
  where b = 0
        b = 1

You can still set a local constant to a non-deterministic and/or partial expression. The meaning is like this:

  let x = (a; b; ... ) in body
= (let x = a in body); (let x = b in body); ...

  let x = ∅ in body
= ∅

It is similar to function application: let x = rhs in body behaves like (\x -> body) rhs. This is why you may find it obvious.

Example:

  let n = luckyNumber  in  (n, n)
= let n = (7; 8) in (n, n)
= (let n = 7 in (n, n)); (let n = 8 in (n, n))
= (7,7); (8,8)

Compare to:

  (luckyNumber, luckyNumber)
= ( (7; 8), (7; 8) )
= (7,7); (7,8); (8,7); (8,8)

Pattern Matching And Guards

Recall pattern matching in Haskell: Commits to first matching clause, latter clauses ignored even if they would match.

But in Curry: All matching clauses are taken, you get multiple answers—non-determinism again.

Example:

insert x ys     = x : ys
insert x (y:ys) = y : insert x ys

If the input list is non-empty, it matches both patterns, so both clauses participate in the answer multiset.

  insert 1 (2:3:[])
= 1:2:3:[] ; 2:insert 1 (3:[])
= 1:2:3:[] ; 2:(1:3:[] ; 3:insert 1 [])
= 1:2:3:[] ; 2:1:3:[] ; 2:3:insert 1 []
= 1:2:3:[] ; 2:1:3:[] ; 2:3:1:[]

There is a way to regain Haskell deterministic first-match-only semantics: Use a case expression.

prepend x xs = case xs of
    ys   -> x : ys
    y:ys -> y : insert x ys   -- this is dead code

Recall guards in Haskell: Commits to first satisfied clause, latter clauses ignored.

In Curry, you can choose that or non-determinism depending on how you write it.

signExclusive x | x >= 0 = "non-neg"
                | x <= 0 = "non-pos"
-- meaning: else-if
-- signExclusive 0 has just one answer "non-neg"

sign x | x >= 0 = "non-neg"
sign x | x <= 0 = "non-pos"
-- meaning: two independent if's
-- sign 0 has two answers, "non-neg" and "non-pos"

Convenience Operators

The standard library provides some non-deterministic operators for convenience.

-- These are in the standard library.

(?) :: a -> a -> a
x ? _ = x
_ ? y = y
-- Binary non-deterministism operator.
-- Example: I could have defined luckyNumber by: luckyNumber = 7 ? 8

failed :: a
-- Always no answer. Identity of (?), e.g., failed ? 1 = 1.

(&>) :: Bool -> a -> a
True &> x = x
-- Note no answer i.e. ∅ for False &> x.
-- Example: `foo | cond = e" can be written as "foo = cond &> e".

(&) :: Bool -> Bool -> Bool
True & True = True
-- Difference from (&&):
--   False && x, x && False are False
--   False &  x, x &  False are no answer, i.e., ∅

Unification

Curry allows asking the computer to find x, y, ys such that, e.g., x : x : y : [] is structurally equal to 1 : y : ys. Technical term: “this unifies with that”; the general task is called “unification”.

unificationExample | x : x : y : [] =:= 1 : y : ys = (x, y, ys)
  where
    x, y, ys free  -- "free" means unknown(s) to be solved for

The computer figures out (1, 1, [1]) because x must be 1, y must be x, and ys must be y : [].

The (=:=) operator gives True if the equation can be solved, else no answer (∅, not even False). Here an example of no answer:

unificationExample0 :: Int
unificationExample0 | x : [] =:= [] = x
  where
    x free

You can think “pattern matching on steroid”. Here is how unification is more powerful:

• Pattern matching compares only a pattern (has unknowns) vs a value (no unknowns). Unification allows unknowns on both sides.

• An unknown can occur only once in pattern matching. Unification allows an unknown to occurs multiple times (e.g., my x), even on both sides (e.g., my y).

However, Curry unification still does not solve arithmetic such as x + 5 =:= 7. It is most effective with algebraic data types, for which it only needs to match up data constructors. E.g., it merely decomposes my example equation into 3 smaller equations:

• x =:= 1
• x =:= y
• y : [] =:= ys

Then the solution is “obvious”.

With Non-Determinism

Non-determinism distributes over unification: If a sub-expression has multiple answers, e.g., luckyNumber, then split into multiple universes, and perform unification in each. Example:

unificationExample2 :: (Int, Int, [Int])
unificationExample2 | x : x : y : [] =:= luckyNumber : y : ys = (x, y, ys)
  where
    x, y, ys free

That leads to two answers, one from x : x : y : [] =:= 7 : y : ys, the other from x : x : y : [] =:= 8 : y : ys.

No Infinite Data

Unification dislikes infinite data, e.g., for xs =:= 0 : xs, the computer declares no answer, rather than giving an infinite-list answer. Technical term: It fails the “occurs-check”, since xs occurs in 0 : xs.

occursCheckExample :: Bool
occursCheckExample = xs =:= 0 : xs
  where
    xs free

Simple Model, Extended for Unification

My model needs to be extended to track unknowns in unification. For each element in a multiset, I append “with x = ?” if x is unsolved, or “with x = 1” if x is solved.

Reasoning example:

  unificationExample2
= x : x : y : [] =:= luckyNumber : y : ys &> (x, y, ys)  with x=?, y=?, ys=?
= x : x : y : [] =:= 7 : y : ys &> (x, y, ys)            with x=?, y=?, ys=? ;
  x : x : y : [] =:= 8 : y : ys &> (x, y, ys)            with x=?, y=?, ys=?
= x=:=7 & x=:=y & y:[]=:=ys &> (x, y, ys)                with x=?, y=?, ys=? ;
  x=:=8 & x=:=y & y:[]=:=ys &> (x, y, ys)                with x=?, y=?, ys=?
= x=:=7 & x=:=y & y:[]=:=ys &> (x, y, ys)                with x=7, y=x, ys=y:[] ;
  x=:=8 & x=:=y & y:[]=:=ys &> (x, y, ys)                with x=8, y=x, ys=y:[]
= True &> (x, y, ys)                                     with x=7, y=x, ys=y:[] ;
  True &> (x, y, ys)                                     with x=8, y=x, ys=y:[]
= (7, 7, 7:[]) ;
  (8, 8, 8:[])

Inverse Queries

With Peano (unary) arithmetic as an example, so I have an algebraic data type for unification to do something:

data N = Z | S N deriving (Ord, Eq, Show)

two = S (S Z)

add Z n = n
add (S m) n = S (add m n)

Can ask inverse-function questions:

• Find x such that add x Z is two: add x Z =:= two where x free
  Computer figures out x = S (S Z)

• Find y such that add (S Z) y is two: add (S Z) y =:= two where y free
  Computer figures out y = S Z

• Find x, y such that add x y is two: add x y =:= two where x,y free
  Computer figures out all 3 answers.

I will show a short example add x Z =:= S Z. The extra rule you need: Evaluating add x Z requires instantiating x to Z or S m (m becomes a new unknown) non-deterministically.

       add x Z =:= S Z    with x=?
=      add x Z =:= S Z    with x=Z        ;
       add x Z =:= S Z    with x=S m, m=?
=            Z =:= S Z    with x=Z        ;
   S (add m Z) =:= S Z    with x=S m, m=?
=  S (add m Z) =:= S Z    with x=S m, m=?
=      add m Z =:= Z      with x=S m, m=?
=            Z =:= Z      with x=S m, m=Z          ;
  S (add m2 Z) =:= Z      with x=S m, m=S m2, m2=?
=              True       with x=S m, m=Z

The standard list concatenation operator (++) is implemented in an analogous wayas add, and so queries like x ++ y =:= [1,2] where x,y free work similarly.

Delimiting Non-Determinism

Sometimes it is useful to limit non-determinism in a local scope, and from the outside you ask:

• Is the multiset of answers empty or non-empty?
• Is x an element?
• Give the minimum/maximum answer.
• Give the sorted list of answers.
• Fold over the answers with a commutative associative operator.

This is supported by the module Control.Search.SetFunctions.

On one side, it converts non-deterministic constants/functions to deterministic constants/functions but the output is the whole multiset:

set0 :: a -> Values a                         -- For constants.
set1 :: (a -> b) -> a -> Values b             -- For 1-ary functions.
set2 :: (a -> b -> c) -> a -> b -> Values c   -- For 2-ary functions.
etc., up to 7

Values is an abstract type for the whole multiset.

On the other side, there are operations for the questions I asked:

isEmpty  :: Values a -> Bool
notEmpty :: Values a -> Bool
valueOf :: Eq a => a -> Values a -> Bool
minValue :: Ord a => Values a -> a
minValueBy :: (a -> a -> Ordering) -> Values a -> a
-- Likewise for max
sortValues :: Ord a => Values a -> [a]
sortValuesBy :: (a -> a -> Bool) -> Values a -> [a]
foldValues :: (a -> a -> a) -> a -> Values a -> a
mapValues :: (a -> b) -> Values a -> Values b

Example: First I have a non-deterministic function decomp3 for decomposing a Peano number into a sum of 3 numbers, each at least 1. Then I can use it to define decomp3Exists for just whether a way exists, decomp3Count for how many, and decomp3s for the sorted list of all decompositions.

decomp3 :: N -> (N, N, N)
decomp3 n | n =:= add (add x y) z = (x, y, z)
  where
    x = S x0
    y = S y0
    z = S z0
    x0, y0, z0 free

decomp3Exists n = notEmpty (set1 decomp3 n)
-- Faster than `decomp3Count n > 0` because notEmpty terminates as soon as
-- an answer is found.

decomp3Count n = foldValues (+) 0 (mapValues (const 1) (set1 decomp3 n))
-- Faster than `length (decomp3s n)` because no sorting done.

decomp3s n = sortValues (set1 decomp3 n)

Question: Why does Curry hesitate to just give you the list of answers in the order they were generated?

Answer: Curry is being purist. Ideally, the generation order is an implementation detail and should not matter, i.e., you should not be able to write code that depends on the exact order.

Logic Programming

Ideal premise of logic programming: You have predicates (as in B36) formalizing your problem, and you implement them by writing their axioms; then you can ask the computer two kinds of questions: whether a predicate is true given arguments; what arguments make it true.

If you have functions in mind, then convert them into predicates like in B36: Define a predicate F(x,y) to represent the sentence f(x)=y. Example: My add function becomes this predicate defined inductively by two axioms:

Add(Z, n, n)
Add(S m, n, S k) ⇐ Add(m, n, k)

Curry goes the reverse direction: It starts with non-deterministic functions and inverse queries. If you have predicates in mind, then convert them into non-deterministic functions by a bias: Choose one argument to become the “output”. (Which to choose depends on the problem.)