CSE341 -- 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:

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 available on the instructional linux cluster (ceylon, fiji, sumatra, tahiti). 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

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, if 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) , if x<y
                     = y : my_merge a b , if 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

Miranda uses Milner-style polymorphism (which was originally developed for type checking 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, universal polymorphism is just right. It isn't what we want for functions -- but Miranda fudges this with a runtime type check. Miranda avoids the complexities of overloading by having a single type num rather than integer and float types. (Haskell's type system includes type classes, which address both of these issues at the cost of added complexity.)

Universal polymorphism doesn't work well at all 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. (F-bounded polymorphism is a way to provide this.)

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::num->num

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
Here * and ** are type variables. (Aside: the * convention for naming type variables is not ideal when the types become complex - it would be better to have names formed using ordinary letters, perhaps with a special marker to distinguish type variables from ordinary variables.)

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 ::= MyInt num | MyBool bool

|| negate a number or apply not to a boolean
flip MyInt n = MyInt (0-n)
flip MyBool b = MyBool (~b)

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]