Re: Narrowing vs. rewriting

From: Michael Hanus <hanus_at_I2.Informatik.RWTH-Aachen.DE>
Date: Fri, 4 Jul 1997 14:20:45 +0200

Philip Wadler wrote:
> I don't find either Sergio's and Harold's examples very convincing,
> as both are easy to program in Haskell. I'm sure there are examples
> of programs that are easy to write in Curry but not so easy to write in
> Haskell, let's see some please! Cheers, -- P

As long as one considers only Herbrand terms and equational
constraints between Herbrand terms, it is difficult to convince
functional programmers, since there are also functional programming
techniques to deal with partial information (lazy evaluation, lambda
abstractions). Nevertheless, I try one. What's about the following
Curry program which implements a type checker for lambda expressions:

  data Expr = Num Int | Var String | App Expr Expr | Lam String Expr
  
  data Texpr = Inttype | Functype Texpr Texpr
  
  tc :: [(String,Texpr)] -> Expr -> Texpr
  tc env (Num _) = Inttype
  tc env (Var v) = lookup env v
  tc env (App e1 e2) | {Functype t1 t2 = tc env e1, t1 = tc env e2} = t2
  tc env (Lam v e) = Functype tv (tc ((v,tv):env) e)
  
  lookup ((v,tv):env) var = if v==var then tv else lookup env var

Expressions are represented as terms of type "Expr", and for
type expressions (Texpr) I assume only an integer and a function
type, but this can be easily extended to other basic types.
The typecheck function "tc" takes an environment for known
variables (represented by lists of pairs of variable names and
type expressions) and an expression and yield the most general
type of this expression. This program runs well in Curry and
produces the following results:

tc [] (Lam "x" (Var "x")) --> Functype a a
tc [] (App (Lam "x" (Var "x")) (Num 3)) --> Inttype


I don't know how an equivalent Haskell program would look like,
since unification is essential here.


However, to obtain real advantages over functional languages,
we should look at constraint programming examples. These are
the killer applications of LP, but as John already pointed out,
LP is a bit low level from a SE point of view. Thus, FLP can
add to LP the same as Haskell or SML adds to imperative
languages: better abstractions, more reliable programs and
avoidance of "dirty" features. To give a concrete example,
the following Curry program can solve constraints in a electrical
network, where the network can contain resistors, serial and
parallel connections (here we assume that a constraint solver
for solving real constraints a la CLP(R) is connected to Curry,
and $+ and $* denote addition and multiplication in this constraint
structure):

  data Network = Resistor Float
                 | Series Network Network
                 | Parallel Network Network

  circuit :: Network -> Float -> Float -> Constraint
  circuit (Resistor r) v i = {v = i $* r}
  circuit (Series n1 n2) v i = {i = i1, i = i2, v = v1 $+ v2,
                                  circuit n1 v1 i1, circuit n2 v2 i2}
  circuit (Parallel n1 n2) v i = {v = v1, v = v2, i = i1 $+ i2,
                                  circuit n1 v1 i1, circuit n2 v2 i2}

The equations for circuit describe the laws of Ohm and Kirchhoff.
Now we can compute the current in a network of two resistors
for a voltage of 5.0:

circuit (Series (Resistor 180.0) (Resistor 470.0)) 5.0 i
--> {i = 0.007692307692307693}

But we can also compute the relationship between several unknown values:

circuit (Series (Series (Resistor r) (Resistor r)) (Resistor r)) v 5.0
--> {r = 0.06666666666666667$*v}

I suppose that it is not so easy to obtain similar results in Haskell.
If I am wrong, please show me the Haskell code.
Of course, I assume a constraint solver which could also be added
to Haskell (indeed, constraint solvers have also been added to C).
However, the important point here is that the presence of logical
variables provides a natural interface of functional (user-defined)
calculations and constraint solving.

Best regards,

Michael
Received on Fri Jul 04 1997 - 15:25:00 CEST

This archive was generated by hypermail 2.3.0 : Wed Sep 18 2019 - 07:15:04 CEST