Curry

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

I will be able to explain logic programming after we understand Curry!

Laziness, Non-Strictness

Curry is lazy and non-strict like Haskell:

four = (\_ -> 4) (div 1 0)   -- 4, no error, div 1 0 ignored.
five = let e = div 1 0 in 5  -- 5, same reason. similarly "where".

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

Non-Determinism

Curry supports non-determinism. This means that an expression can have any number of answers, such as multiple answers or no answers. The following will make it concrete.

Multiple Answers

Functions (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.

Model:

• Think of a multiset of answers. (Even better: Doctor Strange in the Marvel Cinematic Multiverse of Madness. 😈)
• Function application: Apply function to every element in input multiset. (This is for eager/strict functions. Read on for lazy/non-strict functions.)
• Flatten nested multisets.
• My notation for multiset: “x ? y ? …”. The “?” operator has very low precedence, and it is associative because of the flattening. (The standard library provides the same operator with the same meaning.)

Example:

But if the function disregards the argument, then non-determinism in the argument is also disregarded. Example: (\_ -> 4) luckyNumber is deterministic.

What if a strict function uses the same argument multiple times? Then reuse happens, i.e., the non-determinism is not cloned. This example shows what I mean:

Note that it’s different from (luckyNumber,luckyNumber): 4 answers: (7,7), (7,8), (8,7), (8,8), becaue the two occurences of luckyNumber are expanded independently:

Curry docs recommend thinking of luckyNumber (generally top-level non-deterministic constants) as non-deterministic functions of arity 0. Then (luckyNumber,luckyNumber) is just each call site getting its own non-determinism independently.

No Answers

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

secondElement (_ : x : _) = x
-- E.g., secondElement [a,b] = b
-- No answer if the input list is too short, e.g., secondElement [a].

restrictEven n | mod n 2 == 0 = n
-- No answer if n is odd.

E.g., restrictEven 7 outputs no answer.

Model: the empty multiset. My notation: ∅. It becomes the identity of “?”, i.e., x ? ∅ = x, and ∅ ? x = x.

Reasoning example:

This aspect is different from Haskell. In Haskell, restrictEven 7 is ⊥, and causes a runtime error if evaluated. In Curry, it just means the set of answers is empty, which is not considered an error.

More model: Applying an eager/strict function to a ∅ argument gives ∅. Example:

But if the function disregards the argument, then ∅ from the argument is also disregarded. Example:

Pattern Matching And Non-Determinism

General rules for pattern matching:

• All matched branches are taken. (Compare to Haskell: Only the first matched branch is taken.)
• If no match at all, no answer. (Compare to Haskell: ⊥, then runtime error if evaluated.)

Previous examples and new examples:

offByOne n = n + 1
offByOne n = n - 1
-- Both taken because both branches always matched.

secondElement (_ : x : _) = x
-- No answer if the input list is too short.

insert x ys     = x : ys
insert x (y:yt) = y : insert x yt
-- Both branches taken if non-empty list.

-- fcase is the expression version of non-det pattern matching.
-- So insert_V2 is the same as insert.
insert_V2 x lst = fcase lst of
    ys   -> x : ys
    y:yt -> y : insert_V2 x yt

In insert and insert_V2, a non-empty list matches both patterns, so both branches participate in the answer multiset. After expanding the recursion, you get insertion at any position. Example:

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

prepend x lst = case lst of
    ys   -> x : ys
    y:yt -> y : prepend x yt   -- this is dead code

Guards And Non-Determinism

General rules for guards:

• All satisfied branches are taken. (Compare to Haskell: Only the first is taken.)
• If none satisfied, no answer. (Compare to Haskell: ⊥, then runtime error if evaluated.)

Previous example and new example:

restrictEven n | mod n 2 == 0 = n
-- No answer if n is odd.

sign x | x >= 0 = "non-neg"
sign x | x <= 0 = "non-pos"
-- meaning: two independent if's, non-determinism if both true
-- sign 0 = "non-neg" ? "non-pos"

There is a way to regain Haskell deterministic first-satisfied-only semantics: Group multiple guards together:

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

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., ∅

Local Constants

Local constants are treated differently from global constants; the intention is to make the language simpler.

A local constant cannot have multiple definitions:

-- This is a compile-time error.
myTuple_let = let n = 7
                  n = 8
              in (n, n)

But you can still have non-determinism: Use a non-deterministic expression:

-- But you can do this.
myTuple_let = let n = luckyNumber
              in (n, n)

Then it is similar to function application: let x = rhs in body behaves like (\x -> body) rhs.

More examples for the other 3 scenerios: If rhs is ∅; if body disregards the local definition. (They are all similar to function application.)

Non-Determinism Use Case Example

I have some records of students, courses taken, and years taken. I model them as a non-deterministic function from students to courses-years. (There are other ways; I chose this way as an example.)

course "Amani" = ("CSCA67", 2024)
course "Amani" = ("CSCB36", 2025)
course "Amani" = ("MATB24", 2026)
course "Jayce" = ("MATB24", 2026)
course "Karen" = ("CSCB36", 2025)
course "Karen" = ("MATB43", 2025)

I can make a function that finds courses that a student took up to a certain time. It uses a partial function check to check the years.

pastCourse upTo student = check (course student)
  where
    check (crs, yr) | yr <= upTo = crs

E.g., pastCourse 2025 "Amani" gives two answers: CSCA67 and CSCB36.

Unification

Curry allows asking the computer to find x, y, ys such that 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 is an example of no answer:

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

Unification is less magical than it sounds. 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.

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

However, it 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 and recurse on fields. E.g., it merely decomposes my example equation into 3 smaller equations and-ed together with &:

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

Then the solution is “obvious”.

(& is used instead of && because if a smaller equation cannot be solved, we should get no answer instead of False.)

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

With Non-Determinism

Unification distributes over non-determinism: 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.

Model

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.

Example:

Use Case Example

I want to find in which year(s) Karen takes CSCB36; generally given a student and a course, find which year(s).

My course function takes only the student and gives all course-year pairs. But I can unify each pair with (course wanted, year unknown) to limit to the course I want and discover the year(s)!

yearOf :: String -> String -> Int
yearOf student crs | course student =:= (crs, yr) = yr
  where yr free

Reasoning example with Karen and CSCB36:

With that solved, you may now wonder if we can do reverse lookups: Given course and/or year, find students. That will be the next section!

Inverse Queries

Curry can compute some function inverses. This is less magical than it sounds. If your function is defined by pattern matching, then Curry just uses non-determinism and tries every pattern. And if a pattern contains variables, they just become new unknowns to be solved.

Example: Who take CSCB36, and in which years in each case?

course s =:= ("CSCB36", yr) where s, yr free

How the computer figures it out (I omit some easy steps):

Recursive Example: Peano Addition

I define an algebraic data type for Peano (unary) arithmetic:

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

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

I will show two short examples of inverse queries:

• add (S Z) y =:= S (S Z) where y free

  	add (S Z) y =:= S (S Z)	with y = _
  =	S (add Z y) =:= S (S Z)	with y = _
  =	add Z y =:= S Z	with y = _
  =	y =:= S Z	with y = _
  =	True	with y = S Z

• add x Z =:= S Z where x free

  		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 = _)
  =		∅
  	?	(add m Z =:= Z	with x = S m, m = _)
  =		(add m Z =:= Z	with x = S m, m = _)
  =		(add m Z =:= Z	with x = S m, m = Z)
  	?	(add m Z =:= Z	with x = S m, m = S m2, m2 = _)
  =		(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 way as add, and so queries like x ++ y =:= [1,2] where x,y free work similarly.

Delimiting Non-Determinism

Sometimes we want to step outside a non-deterministic program and ask these questions about the answer set:

• Is the multiset of answers empty or non-empty?
• Is one of the answers x?
• 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, you can convert non-deterministic constants/functions to deterministic constants/functions but the output is the whole multiset:

set0 :: a -> Values a                         -- For global 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:

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]  -- use your own LEQ
foldValues :: (a -> a -> a) -> a -> Values a -> a
mapValues :: (a -> b) -> Values a -> Values b

Examples: Using set2 on yearOf, I can ask whether a student takes a course at least once, or count how many times. Using set1 on course, I can enumerate all courses-years a student takes.

-- Does the student take the course at least once?
takesCourse :: String -> String -> Bool
takesCourse student crs = notEmpty (set2 yearOf student crs)

-- How many times the student takes the course
takesCourseTimes :: String -> String -> Int
takesCourseTimes student crs =
    foldValues (+) 0 (mapValues (const 1) (set2 yearOf student crs))

-- List of courses-years the student takes.
coursesYears :: String -> [(String, Int)]
coursesYears student = sortValues (set1 course student)

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 write code that depends on the exact order.

Logic Programming

Since Curry supports non-deterministic functions and inverse queries, the distinction between arguments and return values is blurred. Perhaps some of those non-deterministic functions actually represent predicates, in the following sense.

Recall my course and pastCourse functions:

course "Amani" = ("CSCA67", 2024)
course "Amani" = ("CSCB36", 2025)
etc.

pastCourse upTo student = check (course student)
  where
    check (c, y) | y <= upTo = c

course stands for the following predicate enrol for who takes which courses and when, defined by listing what arguments make it true (and implicitly false otherwise)—you can think axioms.

enrol("Amani", "CSCA67", 2024)
enrol("Amani", "CSCB36", 2025)
etc.

pastCourse stands for the following predicate pastEnrol for who takes which courses up to a certain time, defined by an axiom that uses enrol with a check on the year:

pastEnrol(upTo, student, c) ⇐ enrol(student, c, y) ∧ y ≤ upTo

(It’s customary to just say “⇐” because, again, we just state how to make a predicate true; then it is implicitly false otherwise.)

Generally, a non-deterministic function f can stand for a predicate p (or vice versa) under this convention: f(x) gives an answer y iff p(x,y) is true.

Logic programming refers to defining predicates rather than functions. You can then ask the computer whether a predicate is true for the arguments you supply; you can also leave some arguments as unknown variables, and the computer will try to solve for them. (The computer just tries exhautive search and unification.) Here are some examples:

What Curry does is functional logic programming, i.e., you write non-deterministic functions, but conceptually they can stand for predicates, and you can do everything that logic programming does.