Begginer looking to provide a default parameter without changing the signature of a function

Learning
1

Hi!

I’m just starting out so please let me know if I’m doing anything particularly silly:

I have defined a function:

let try_next ~f s = 
    try Some (Stream.next s |> f) 
    with Stream.Failure -> None
;;
val try_next : f:('a -> 'b) -> 'a Stream.t -> 'b option = <fun>

But when I try to provide the identity function as a default for f I find that the signature for the function changes; presumably because the type-checker can see that Fn.id is of 'a -> 'a:

let try_next ?(f=Fn.id) s = 
    try Some (Stream.next s |> f) 
    with Stream.Failure -> None
;;
val try_next : ?f:('a -> 'a) -> 'a Stream.t -> 'a option = <fun>

Even trying to supply my own signature (the original) is taken as a mismatch:

module StreamEx : sig
   val try_next : ?f:('a -> 'b) -> 'a Stream.t -> 'b option
end = struct
    let try_next ?(f=Fn.id) s = 
        try Some (Stream.next s |> f) 
        with Stream.Failure -> None
end
;;
Error: Signature mismatch:
    ...
    Values do not match:
     val try_next : ?f:('a -> 'a) -> 'a Stream.t -> 'a option
    is not included in
     val try_next : ?f:('a -> 'b) -> 'a Stream.t -> 'b option

Any help would be appreciated.

2

The short answer is that is not possible to have a different types for the optional argument depending if the argument is explictely provided or not; and your default case has for type 'a->'a and not 'a->'b. At the type level, optional arguments are a form of typing sugar over argument with an 'a option type. In other word, a function like

let filter ?map pred l = match map with
  | None -> List.filter pred l
  | Some map -> List.filter (fun x -> pred (map x)) l

is equivalent at the type level to

let filter (map: ('a -> 'b) option) (pred:'b -> bool) (l:'a list): 'a list =
  match map with
  | None -> List.filter pred l
  | Some map -> List.filter (fun x -> pred (map x)) l

And when the type-checker types the first branch of the pattern matching , it sees that pred is used as an argument of filter, therefore pred:'a -> bool and 'a ≡ 'b. It is therefore impossible to use optional argument when the type of the None case should be different than the type of the Some x branch.

Nevertheless, a more complete answer should mention that with GADTs it is possible to refine the type of the scrutinee on a case by case basis in a pattern matching. It is therefore possible to make the previous function typechecks by introducing a new optional type:

 type ('generic,'default) optional =
 | Default: ('default,'default) optional
 | Specific: 'generic -> ('generic,'default) optional

With this type enhanced with more type information than the standard option type, one can rewrite filter as

  let filter (type a b) (map: (a -> b, a -> a ) optional) (pred:b -> bool) (l:a list)
     : a list = match map with
  | Default -> List.filter pred l
  | Specific map -> List.filter (fun x -> pred (map x)) l

This function is accepted by the type-checker. Nevertheless, without the optional argument mechanism, it is not very useful by-itsef.

Extending the existing optional argument mechanism to work with this kind of GADT-ladded option is not very hard at a first glance. However, that would mean that GADTs related type errors will seep into these enhanced optional arguments: code generation plus GADT errors do sound like they have the potential to be very confusing together.

1 Like
3

Thanks for your detailed reply. I can’t say I really followed the section on GADTs as I don’t really understand what they are for yet.

However from what I understand of what you said at the beginning, it is somewhat surprising to me that this is not a relatively straight forward. My naive intuition on the type inference would have been that the signature (where the function is given the default of Fn.id : 'a -> 'a:

 val try_next : ?f:('a -> 'a) -> 'a Stream.t -> 'a option

Is a subset of the more general case:

 val try_next : ?f:('a -> 'b) -> 'a Stream.t -> 'b option

Where 'a = 'b, and therefore it should just be a case of giving the type checker the hits it needs to say that I am in fact expecting the general case even though the default function I am supplying fits the specific case. I’m not sure I’m seeing the significance of an optional argument in fact going through an option behind the scenes, other than it’s another layer of abstraction that the type-checker is having to deal with.

I think a better version of your example would be if the None pattern match section took a second map : 'a -> 'b which in practice was being given a map function that implemented map so that b' = 'a

But, since you are saying it’s not possible I the best way I can think to deal with it is just to partially apply the identity function, so that I have something like:

let try_next_map ~f s = 
    try Some (Stream.next s |> f) 
    with Stream.Failure -> None
let try_next s = try_next_map ~f:Fn.id s
;;
val try_next_map : f:('a -> 'b) -> 'a Stream.t -> 'b option = <fun>
val try_next : 'a Stream.t -> 'a option = <fun>