In imperative languages, variables are abstract versions of memory
locations. We can read and write them (using assignments). There is no
referential transparency -- if we have an assignment statement
x := y+3 we are not necessarily allowed to substitute
y+3 for every occurrence of x in the program.
In mathematics, we can substitute equals for equals: if x=y+z then we can substitute y+z for x.
Interesting stuff about Miranda:
To run Miranda:
lynx% mira or lynx% mira myprog.m to load file "myprog.m"See ~borning/miranda/* on lynx for sample programs -- all the examples in these lecture notes are on lecture.m
Interactive environment (like Lisp)
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 FalseDefining a function:
double x = x+x
|| recursive factorial
rec_factorial n = 1, n=0
= n * rec_factorial (n-1), n>0
|| factorial using the built-in prod function
factorial n = product [1..n]
|| mapping function, like mapcar in Lisp
my_map f [] = []
my_map f (a:x) = f a : my_map f x
Using the factorial function:
factorial 3 my_map factorial [1,5] my_map factorial [1..10] my_map factorial [1..]
/man - online manual /help /edit - edit your program; reload on exit from editor /quit (or control d)
data types:
Functions are first class citizens -- we can pass them as arguments, and return them as values from other functions
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]
plus x y = x+y f = plus 1 ff = (+) 1 twice f x = f (f x) g = twice f g 3
hyp x y = sqrt sum
where sum = x*x + y*y
Curious design feature: block structure is indicated by indentation rather
than by keywords such as begin and end.
twice f x = f (f x)
double = (*) 2
twice double 4
map f [] = []
map f (a:x) = f a: map f x
map double [1..5]
argument and result types of function can be different:
map code "0123"
[48,49,50,51]
const k x = k
sum [] = 0
sum (a:x) = a+sum x
my_filter f [] = []
my_filter f (a:x) = a : my_filter f x, f a
= my_filter f x, otherwise
interesting uses:
member x a = or (map (=a) x)
length x = sum (map (const 1) x)
A polymorphic function is a function with a type variable in its type
|| the :: asks for the type of an expression 3:: num [1,2,3] :: [num] [[1,2,3]] :: [[num]] []:: [*] neg :: num -> num + :: num -> num -> num (note that -> is right associative) member:: [*] -> * -> bool = :: * -> * -> boolrun time error if = applied to functions
How does type checking work? Type variables are logic variables as in Prolog. We use unification to build up information about types.
double x = x+x 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 xIn Milner-style polymorphism there are no restrictions on the types that a type variable can take on. (This is also called universal polymorphism.)
As a result of this restriction the type system not always as descriptive as one would like. For functions such as append and member, it's just right. However, the situation becomes impossible for object-oriented languages: there want a type system that can specify (for example) that a variable x can hold any object that understands the + and * messages.
Definitions: we've been discussing polymorphic functions. A related concept is an overloaded function. (Miranda doesn't have these, but other languages do.) An overloaded function is a function with several different definitions. The compiler (or maybe the runtime system) selects which function is required based on the types of the arguments. Example: + in Algol, Pascal, and Ada; user-defined overloaded functions in Ada.
There are different types for each overloaded function definition.
Polymorphic functions are different -- there is a single function definition, with a polymorphic type (not multiple functions with different types).
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 Lisp:
(setf ones '(1))
(nconc 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) , xa ]
|| 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), ...
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 q1However, this won't work:
q1 = [3,5]