CSE 341 -- Miranda

Miranda is an example of a pure functional programming language -- there are no side effects.

Imperative languages have variables and assignment; they are in effect abstractions of the von Neumann machine. There is no referential transparency.

In mathematics, we can substitute equals for equals:
if x=y+z then you can substitute y+z for x

Informally, in a referentially transparent language you can substitute equals for equals, just as in mathematics.

Interesting features of Miranda:

truly functional
lazy evaluation -- can deal with infinite structures
type system -- statically typed, no type declarations needed; polymorphic
combinator-based implementation

Haskell is a standard pure functional language, but it is much more complex than Miranda. ML has a functional subset.

future of functional languages ...?
barriers:

Running Miranda

The system is only available on orcas (we just bought a one-system license). To run it, type

mira

To load in an existing file named myfile.m, type

mira myfile.m

For a list of useful commands within Miranda type /help. These include the ability to edit the current program (or script, to use Miranda terminology). To do this, type /edit. The newly edited script is then loaded in. Other commands:

/man  - online manual
/quit (or  control d)

The default editor is vi, but you can change this by adding the following line to your .cshrc file:

setenv EDITOR /usr/local/bin/emacs

Miranda is an interactive tty-oriented environment (like Scheme). Examples:

Miranda  3+4
  7

Miranda  8 : [1..10]
  [8,1,2,3,4,5,6,7,8,9,10]

Miranda  [1,2,3] ++ [8,9]
  [1,2,3,8,9]

Miranda  member [1,2,3] 8
  False

To define a function:

double x = x+x

Function and other definitions must go in a file (script); Miranda distinguishes between definition mode (when reading from a file) and evaluation mode.

Data types

numbers (both int and float): 3 4.5 3.9e10
booleans: True False
characters: 'a'
lists: [1,2,3,8]

type system requires that all elements in a list must be of the same type:

  [2,4,7]
  [[1,2],[4,9]]

strings -- shorthand for list of chars "hi there"

tuples: (False,[1,2,3],"str")

functions are first class citizens

function application denoted by juxtaposition

neg 3
-3
member [1,4,6] 4

infix -- 
3+4
(+) 3 4

arithmetic 
+ - * /
sin cos etc
sum, product

product [1,2,8]

Recursion Examples

Miranda is quite terse. See ~borning/miranda/* on orcas for example programs (or scripts). All the examples in these lecture notes are on lecture.m

|| recursive factorial
|| whitespace is significant - notice the use of layout in the example

rec_factorial n = 1, n=0
                = n * rec_factorial (n-1), n>0

|| alternate version using pattern matching:
pattern_factorial 0     = 1
pattern_factorial (k+1) = (k+1) * pattern_factorial k


|| factorial using the built-in prod function
factorial n = product [1..n]

|| mapping function, like map in Scheme
my_map f [] = []
my_map f (a:x) = f a : my_map f x


my_map factorial [1,5]
my_map factorial [1..10]
my_map factorial [1..]

Currying

plus x y = x+y

f = plus 1

ff = (+) 1

twice f x = f (f x)

g = twice f

g 3

block structure - lexical scoping

hyp x y = sqrt sum
          where sum = x*x + y*y



hyp2 x y = sqrt sum
           where sum = x2 + y2
                       where x2 = x*x
                             y2= y*y

Lazy Evaluation and Infinite Lists

my_if True x y = x
my_if False x y = y

my_if (x>y) 3 4

my_if (x>y) 3 (1/0)

ones = 1 : ones

Compare with circular list in Scheme:

  (define ones '(1))
  (set-cdr! ones ones)

ints n = n : ints (n+1)
[1..]

lets = "abc" ++ lets

Two prime number programs:

factors n = [k | k <- [1..n]; n mod k = 0]

dullprimes = filter isprime [2..]
             where
             isprime p = (factors p = [1,p])


interestingprimes = sieve [2..]
                    where
                    sieve (p:x) = p : sieve [n | n <- x; n mod p > 0]

Hamming numbers:

my_merge (x:a) (y:b) = x : my_merge a (y:b) , x<y
                  = y : my_merge a b , x=y
                  = y : my_merge (x:a) b , otherwise

ham = 1: my_merge ham2 (my_merge ham3 ham5)

ham2 = map (*2) ham
ham3 = map (*3) ham
ham5 = map (*5) ham

higher-order functions

twice f x = f (f x)
double = (*) 2

twice double 4


map f [] = []
map f (a:x) = f a: map f x

map ( (+) 1) [1..5]

argument and result types of function can be different:

map code "0123"
[48,49,50,51]

interesting uses:

member x a = or (map (=a) x)

length x = sum (map (const 1) x)

sum, product, and, or, concat, etc ...

could define recursively, e.g.

sum [] = 0
sum (a:x) = a+sum x


foldr op r = f
             where
             f [] = r
             f (a:x) = op a(f x) 

sum = foldr (+) 0
product = foldr (*) 1
or = foldr (\/) False
and = foldr (&) True

This does not hurt efficiency. Miranda's implementation uses combinator graphs -- the first time you run the function it rewrites that portion of the graph.

This is also the case for things like (1+3) and code '0'

Other examples:

my_filter f [] = []
my_filter f (a:x) = a : my_filter f x, f a
                  = my_filter f x, otherwise

reverse_args f x y = f y x

const k x = k

fix f = e
        where e = f e

double x = 2*x
const x y = x

Type system

Milner-style polymorphism; also used in ML.

A polymorphic function is a function with a type variable in its type. In Milner-style polymorphism there are no restrictions on types that a type variable can take on (universal polymorphism).

3::
num

[1,2,3] ::
[num]

[[1,2,3]] ::
[[num]]

[]::
[*]

neg ::
num -> num

+ ::
num -> num -> num
(note that -> is right associative)

member:: 
[*] -> * -> bool

= ::
* -> *  -> bool

run time error if = applied to functions

The type system is not always as descriptive as one would like.

For append and member, it's just right, but the situation becomes impossible for object-oriented languages: there we want a type system that specifies that a variable x can hold any object that understands the + and * messages ...

How does type checking work?

Variables are like the logic variables we'll encounter in CLP(R). The type checker uses unification (i.e. two-way pattern matching).

Examples:

double x = x+x
double::int->int

map f [] = []
map f (a:x) = f a: map f x

map::(*->**)->[*]->[**]

map code "0123"
[48,49,50,51]


twice:: 
(*->*)->*->*


map f [] = []
map f (a:x) = f a: map f x


foldr::(*->**->**)->**->[*]->**
foldr op r = f
             where
             f [] = r
             f (a:x) = op a(f x) 


sum = foldr (+) 0

User-defined types

numtree ::= EmptyNumTree | NumNode num numtree numtree

t1 = NumNode 7 EmptyNumTree (NumNode 4 EmptyNumTree EmptyNumTree)


|| polymorphic types:

tree * ::= EmptyTree | Node * (tree *) (tree *) 

t2 = Node 7 EmptyTree (Node 4 EmptyTree EmptyTree)



flatten (Node n left right) = flatten left ++ [n] ++ flatten right
flatten EmptyTree = []

This allows enumeration types, union types, variant records:

weekday ::= Mon | Tues | Wed | Thurs | Fri
intbool ::= I num | B bool

string == [char]
token ::= Coeff num | Var string | Exp | Plus | Times

ZF notation (list comprehensions)

a list of cubes of numbers betwen 1 and 10

	[ n*n*n | n <- [1..100] ]

all cubes:

	[ n*n*n | n <- [1..] ]

	perms [] = [[]]
	perms x  = [ a:y | a <- x; y <- perms (x--[a]) ]

|| quicksort

qsort [] = []
qsort (a:x) = qsort [ b | b <- x; b<=a ] ++ [a] ++ qsort [ b | b <- x; b>a ]

Square root
`limit' applied to a list of values, returns the first value which is the same as its successor. Useful in testing for convergence. For example the following Miranda expression computes the square root of r by the Newton-Raphson method

sqt r = limit [x | x<-r, 0.5*(x + r/x).. ]

limit::[*]->*
limit (a:b:x) = a, if a=b
              = limit (b:x), otherwise
limit other = error "incorrect use of limit"


cp x y = [ (a,b) | a <- x; b <- y]

Miranda cp [1..5] [1..4]
[(1,1),(1,2),(1,3),(1,4),(2,1),(2,2),(2,3),(2,4),
(3,1),(3,2),(3,3),(3,4),(4,1),(4,2),(4,3),(4,4),(5,1),(5,2),(5,3),(5,4)]


cpdiag x y = [ (a,b) // a <- x; b <- y]

rats = cpdiag [1..] [1..]

[(1,1),(1,2),(2,1),(1,3),(2,2),(3,1),(1,4),(2,3),(3,2),(4,1),
(1,5),(2,4),(3,3),(4,2),(5,1),(1,6),(2,5),(3,4),(4,3),(5,2),
(6,1),(1,7),(2,6),(3,5),(4,4),(5,3),(6,2),(7,1),(1,8),(2,7),
(3,6),(4,5),(5,4),(6,3),(7,2),(8,1),(1,9),(2,8),(3,7),(4,6),(5,5),
(6,4),(7,3),(8,2),(9,1),(1,10),(2,9),(3,8),(4,7),(5,6),(6,5), ...

force -- forces all parts of its argument to be evaluated

other functional languages that don't use combinators -- more conventional approach to lazy evaluation would be to pass a thunk

there, strictness analysis can win big in efficiency

Abstract data types in Miranda

abstype queue *
    with emptyq :: queue *
         isempty :: queue * -> bool
	 head :: queue * -> *
	 add :: * -> queue * -> queue *
	 remove :: queue * -> queue *
	 
queue * == [*]
emptyq = []
isempty [] = True
isempty (a:x) = False           
head (a:x) = a
add a q = q ++ [a]
remove (a:x) = x

Outside of the definition, the only way you can get at the queue is via its protocol. Example: building a queue

q1 = add 5 (add 3 emptyq)
q2 = remove q1

this won't work: q1 = [3,5]