Define a polymorphic function where output depends on input but with different type parameter

Learning
1

Background

I’ve trying to write some code for a sort-of-like-a-result polymorphic type, and I’d like to hold onto whether we know statically that the type is Ok.

For example, return looks like:

val return : 'a -> 'a ok

And there’s these two functions:

val get : 'a ok -> 'a
val get_exn : 'a t -> 'a

(And there are functions that convert 'a t to 'a ok in some instances)

The idea is that you can only call get if we can statically determine that the contents are Ok; otherwise you have to call get_exn.

End background

So that’s the background, and I’m wondering if it’s possible to write a map (or bind) function that keeps this information. Right now I have:

val map : [< 'a t ] -> f:('a -> 'b) -> [> 'b t ]

But this means the type of return x |> map ~f:Fn.id is x t instead of x ok.

I’d like to write something like:

val map : ([< 'a t] as 'c) -> f:('a -> 'b) -> [> 'c ]

But of course this doesn’t work because 'c uses 'a but we’re actually returning 'b.

So is there a way to make that return type say something like 'c except substitute 'b for 'a?

Bonus points

If there is a way to do this, can I extend this to the type of both?

val both : 'a t-> 'b t -> [> ('a * 'b) t ]
2

This seems like it requires higher-kinded types, which aren’t supported natively. You could use a library like higher_kinded to do something like what you want, but it isn’t going to be terribly ergonomic. You might as well write something like:

module Result_like : sig
  type 'a t
  val get_exn : 'a t -> 'a

  include Monad.S with type 'a t := 'a t

  module Ok : sig
    type 'a t
    val get : 'a t -> 'a

    include Monad.S with type 'a t := 'a t
  end

  val get_ok : 'a t -> 'a Ok.t option
end
3

Keeping the information about the ok part in the type system is quite direct:

type true' = T
type false' = F

type _ t =
  | Ok: 'a -> <ok:'a; error:'b; is_ok:true'> t
  | Error: 'b -> <ok:'a; error:'b; is_ok:false'> t

let return x = Ok x

let get (Ok x) = x

let get_exn: type a b bool. <ok:a; error:b; is_ok:bool> t -> a =
function
  | Ok x -> x
  | Error _ -> raise Not_found

let map (type ok f_ok error bool)
    (f:ok -> f_ok)
    (x:<is_ok:bool; ok:ok; error:error> t)
  : <is_ok:bool; ok:f_ok; error:error > t = match x with
  | Ok x -> Ok (f x)
  | Error y -> Error y

Computing the tag for both looks to be easier using an auxiliary witness:


type (_,_,_) and_witness =
  | Same: ('bool, 'bool, 'bool ) and_witness
  | E1: (false', 'y, false') and_witness
  | E2: ('x, false', false') and_witness


let both (type ok ok2 f_ok error bool1 bool2 and'):
    (ok -> ok2 -> f_ok)
  -> <is_ok:bool1; ok:ok; error:error> t
  -> <is_ok:bool2; ok:ok2; error:error> t
  -> (bool1,bool2,and') and_witness
  -> <is_ok:and'; ok:f_ok; error:error> t
 =
  fun f x y wmax -> match x, y, wmax with
    | Ok x, Ok y, Same -> Ok (f x y)
    | Error x, Error y, Same -> Error x
    | Error x, _ , E1 -> Error x
    | _, Error x, E2 -> Error x

let is_ok (Ok _ as x) = x
let is_error (Error _ as e) = e
let x = is_ok @@ both (+) (Ok 0) (Ok 1) Same
let y = is_error @@ both (+) (Error "wrong") (Ok 2) E1
4 Likes