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

**URL:** <https://discuss.ocaml.org/t/define-a-polymorphic-function-where-output-depends-on-input-but-with-different-type-parameter/5848>\
**Category:** Learning\
**Created:** [May 26, 2020, 6:41pm UTC](https://discuss.ocaml.org/t/define-a-polymorphic-function-where-output-depends-on-input-but-with-different-type-parameter/5848 "2020-05-26T18:41:47Z")\
**Posts on this page:** 3\
**Page:** 1

<div class="post-metadata">

**Author:** ![BrendanLong](https://sea2.discourse-cdn.com/flex020/user_avatar/discuss.ocaml.org/brendanlong/32/522_2.png) [@BrendanLong](https://discuss.ocaml.org/u/BrendanLong)\
**Post date:** [May 26, 2020, 6:41pm UTC](https://discuss.ocaml.org/t/define-a-polymorphic-function-where-output-depends-on-input-but-with-different-type-parameter/5848/1 "2020-05-26T18:41:47Z")

</div>

### 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:

```auto
val return : 'a -> 'a ok

```

And there’s these two functions:

```auto
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:

```auto
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:

```auto
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`?

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

```

---

<div class="post-metadata">

**Author:** ![bcc32](https://sea2.discourse-cdn.com/flex020/user_avatar/discuss.ocaml.org/bcc32/32/203_2.png) [@bcc32](https://discuss.ocaml.org/u/bcc32)\
**Post date:** [May 26, 2020, 7:34pm UTC](https://discuss.ocaml.org/t/define-a-polymorphic-function-where-output-depends-on-input-but-with-different-type-parameter/5848/2 "2020-05-26T19:34:05Z")

</div>

This seems like it requires higher-kinded types, which aren’t supported natively. You could use a library like [higher\_kinded](https://github.com/janestreet/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:

```ocaml
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

```

---

<div class="post-metadata">

**Author:** ![octachron](https://avatars.discourse-cdn.com/v4/letter/o/49beb7/32.png) [@octachron](https://discuss.ocaml.org/u/octachron)\
**Post date:** [May 26, 2020, 9:39pm UTC](https://discuss.ocaml.org/t/define-a-polymorphic-function-where-output-depends-on-input-but-with-different-type-parameter/5848/3 "2020-05-26T21:39:28Z")

</div>

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

```ocaml
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:

```ocaml

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

```