I'm writing a fairly large program in Standard ML and I'm having a
problem with the 'map' function. Any help would be great.
If L is a list, I would like to compute:
map hd L
map (map hd) L
map (map (map hd)) L
... (etc)
I want to write a function in the lines of
fun f 0 = map hd
| f 1 = map (ff 0)
| f 2 = map (ff 1)
| f 3 = map (ff 2)
| f 4 = map (ff 3)
| f k = raise tooHighArity
but this would stop at some point k. I tried to write a general
elegant version
fun f 0 = map hd
| f k = map (ff (k-1))
but got the following error
stdIn:1.5-17.24 Error: right-hand-side of clause doesn't agree with
function result type [circularity]
expression: 'Z list list list -> 'Z list list
result type: 'Z list list -> 'Z list
in declaration:
ff = (fn 0 => map hd
| k => map (ff <exp>))
I was really expecting this to compile. My questions are: (1) what's
wrong with the function I defined? (2) is there anyway to write
function f for arbitrary k to achieve the desired functionality?
Thanks for any help,
Oscar.
(1) It makes no sense. ;-) Just consider evaluating
ff 3
= map (ff 2)
= map (map (ff 1))
= map (map (map (ff 0)))
= map (map (map (map hd)))
And now recall the type of map: ('a -> 'b) -> ('a list -> 'b list) and
construct the type of the latter expression - it won't be what you
want.
(2) Your question is basically unrelated to map. Try:
fun repeat 0 f x = x
| repeat n f x = repeat (n-1) f (f x)
Now you can do:
repeat 10 (map f) xs
- Andreas
That is a limitation of SML's type system. OCaml can handle it if you
enable -rectypes:
# open List;;
# let rec f g = function
| 0 -> map g
| n -> map (f g (n-1));;
val f : (('a list as 'a) -> ('b list as 'b)) -> int -> 'a -> 'b = <fun>
Note the recursive types in the function's signature, e.g. "'a list as 'a".
However, your function is virtually useless because the nested lists cannot
contain values other that more cyclic lists. You can do:
# let rec zero = [] and one = [zero] and many = [many; many];;
val zero : 'a list = []
val one : 'a list list = [[]]
val many : 'a list as 'a =
...
# f (function [] -> one | _ -> zero) 1 many;;
- : 'a list as 'a = [[[]; []]; [[]; []]]
But that is not very useful.
You probably want an explicit nested list or tree data structure instead:
type 'a t = Leaf of 'a | Node of 'a t list
--
Dr Jon D Harrop, Flying Frog Consultancy Ltd.
http://www.ffconsultancy.com/?u
> fun f 0 = map hd
> | f k = map (ff (k-1))
>
> but got the following error
>
> stdIn:1.5-17.24 Error: right-hand-side of clause doesn't agree with
> function result type [circularity]
> expression: 'Z list list list -> 'Z list list
> result type: 'Z list list -> 'Z list
> in declaration:
> ff = (fn 0 => map hd
> | k => map (ff <exp>))
This function has a dependent type. For instance, if you had a type
function:
nest 0 t = t list
nest k t = (nest (k-1) t) list
Which gives you things like:
nest 5 int = int list list list list list list
Then you could type your function as something like:
ff : (n : int) -> nest n ('a list) -> nest n 'a
Note that the type of the of the second argument and the result depends on
the *value* (n) of the first argument.
You can write functions with types like these in Coq, Agda, etc., but ML and
Haskell and the like don't have dependent type systems (although there may
be other ways to write the function; you can write such a 'deep map' as a
type class in Haskell, so maybe there's some way with parameterized modules
you could write it in ML).
-- Dan
> This function has a dependent type.
I should note that you can get away with fairly restricted versions of
'dependent typing' for this particular problem. For instance, in GHC:
--- snip ---
{-# LANGUAGE TypeFamilies, GADTs, EmptyDataDecls #-}
data Z
data S n
data Nat n where
Z :: Nat Z
S :: Nat n -> Nat (S n)
type family Nest n a :: *
type family Nest Z a = [a]
type family Nest (S n) a = [Nest n a]
deepMap :: Nat n -> (a -> b) -> Nest n a -> Nest n b
deepMap Z f = map f
deepMap (S n) f = map (deepMap n f)
--- snip ---
So 'all' you need are:
1) Type-level naturals/data kinds.
2) Type-level functions with pattern matching on the data kinds.
3) GADTs or something similar to make families of singleton types such
that matching on a natural value refines a type-level natural.
So you can do this in, say, Omega and Dependent ML (and GHC, as above), and
don't really need one of the more full-on dependent languages like Coq.
-- Dan