CSE 505 -- 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 available on the instructional linux cluster (ceylon, fiji, sumatra, tahiti). It is also available on orcas - but I'd use the linux boxes since they are faster. 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, 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 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 the same as the logic variables we used in CLP(R). The type checker uses unification (i.e. solving equality constraints over trees).

Examples:

double x = x+x
double::num->num

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

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

Here * and ** are type variables. Aside: the * convention for naming type variables is perhaps not ideal. In Haskell the type of map is written

 (a -> b) -> [a] -> [b]

In ML it is

 ('a -> 'b) -> ['a] -> ['b]

Back to Miranda ...

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 ::= 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]