Can I annotate the complete type of a `fun` declaration?

In a learning environment, what are my options to provide type signatures for functions?

Standard ML doesn't have top-level type signatures like Haskell. Here are the alternatives I have considered:

Module signatures, which require either a separate signature file, or the type signature being defined in a separate block inside the same file as the module itself. This requires the use of modules, and in any production system that would be a sane choice.

Modules may seem a little verbose in a stub file when the alternative is a single function definition. They both introduce the concept of modules, perhaps a bit early,

Using val and val rec I can have the complete type signature in one line:

val incr : int -> int =
  fn i => i + 1

val rec map : ('a -> 'b) -> 'a list -> 'b list =
  fn f => fn xs => case xs of
       []    => []
     | x::ys => f x :: map f ys

Can I have this and also use fun?

If this is possible, I can't seem to get the syntax right.

Currently the solution is to embed the argument types and the result type as such:
```
fun map (f : 'a -> 'b) (xs : 'a list) : 'b list =
  raise Fail "'map' is not implemented"
```
But I have experienced that this syntax gives the novice ML programmer the impression that the solution either cannot or should not be updated to the model solution:
```
fun map f [] = []
  | map f (x::xs) = f x :: map f xs
```
It seems then that the type signatures, which are supposed to aid the student, prevents them from pattern matching. I cannot say if this is because they think that the type signatures cannot be removed or if they should not be removed. It is, of course, a matter of style whether they should (and where), but the student should be enabled to explore a style of type inference.

Solution

By using a let or local bound function, and shadowing you can declare the function, and then assign it to a value.

using local for this is more convenient, since it has the form: local decl in decl end, rather than let decl in expr end, meaning let's expr, wants a top-level argument f

val map = fn f => let fun map = ... in map end

I don't believe people generally use local, anymore primarily because modules can do anything that local can, and more, but perhaps it is worth considering it as an anonymous module, when you do not want to explain modules yet.

local
  fun map (f : 'a -> 'b) (x::rest : 'a list) : 'b list
        = f x :: map f rest
    | map _ ([]) = []

 in
 val (map : ('a -> 'b) -> 'a list -> 'b list) = map;
end

Then when it comes time to explain modules, you can declare the structure inside the local, around all of the declarations, and then remove the local, and try to come up with a situation, where they have coded 2 functions, and it's more appropriate to replace 2 locals, with 1 structure.

local
  structure X = struct
    fun id x = x
  end
  in val id = X.id 
end

perhaps starting them off with something like the following:

exception ReplaceSorryWithYourAnswer

fun sorry () = raise ReplaceSorryWithYourAnswer

local
  (* Please fill in the _'s with the arguments
     and the call to sorry() with your answer *)
  fun map _ _ = sorry ()
in
  val map : ('a -> 'b) -> ('a list) -> ('b list) = map
end