# Detecting identity functions in Flambda

**URL:** <https://discuss.ocaml.org/t/detecting-identity-functions-in-flambda/8180>\
**Category:** Community\
**Tags:** flambda\
**Created:** [July 22, 2021, 8:43am UTC](https://discuss.ocaml.org/t/detecting-identity-functions-in-flambda/8180 "2021-07-22T08:43:01Z")\
**Posts on this page:** 1\
**Showing post:** 2

<div class="post-metadata">

**Author:** ![thierry-martinez](https://sea2.discourse-cdn.com/flex020/user_avatar/discuss.ocaml.org/thierry-martinez/32/1481_2.png) [@thierry-martinez](https://discuss.ocaml.org/u/thierry-martinez)\
**Post date:** [July 22, 2021, 12:40pm UTC](https://discuss.ocaml.org/t/detecting-identity-functions-in-flambda/8180/2 "2021-07-22T12:40:45Z")

</div>

Very nice and interesting work! Congrats to Léo!

The paragraph about “higher-order capabilities” is a bit cryptic for me: is `List.map f` recognized as an identity as soon as `f` is? And what about `Set.Make(X).map` and so on? I think about another approach: instead of requiring to write identity functions between two types `t` and `u`, we could allow `(e : t :> u)` as soon as we can recognize that `t` and `u` share the same memory representation (or, more generally, that every value of `t` has a memory representation that is also valid as a value of `u`). The benefit of coercion is that it naturally allows deep transformations, and I think that it is what @EduardoRFS suggested in [Records, tuples and variants subtyping](https://discuss.ocaml.org/t/records-tuples-and-variants-subtyping/6516), but one of the difficulties is perhaps to recognize that the memory representations of `t` and `u` are compatible. (We can then mix the approaches by allowing coercions between `t` and `u` as soon as we are able to write an identity function between the two types.)

I cannot resist to share a related puzzle… You can check that there should be an identity function `('a, 'b, 'c) plus -> ('a, 'b, 'c) cursor` between the types:

```auto
type zero = [`Zero] and 'a succ = [`Succ of 'a]

type ('a, 'b, 'c) plus =
  | PO : (zero, 'a, 'a) plus
  | PS : ('a, 'b, 'c) plus -> ('a succ, 'b, 'c succ) plus

type ('a, 'b, 'c) cursor =
  | CO : (zero, 'a, 'a) cursor
  | CS : ('a, 'b succ, 'c) cursor -> ('a succ, 'b, 'c) cursor

```

(You can check for instance that for all `n` \>= 0 and for all types `'a, 'b, 'c`, we have `PS^n PO : ('a, 'b, 'c) plus` if and only if `CS^n CO : ('a, 'b, 'c) cursor`.)

However, I have found very difficult to write such an identity function that will not be in quadratic time with respect to the size of its argument (I think I have a linear-time implementation, but it is incredibly convoluted, and in retrospect it could even have been a good candidate for [https://discuss.ocaml.org/t/share-your-crazy-ocaml-code-snippet/8116:](https://discuss.ocaml.org/t/share-your-crazy-ocaml-code-snippet/8116:) I prefer not to share it right now not to spoil if someone wants to search a bit). I don’t know if there is some functions `('a, 'b, 'c) plus -> ('a, 'b, 'c) cursor` for which the approach presented here can prove to be an identity.

---

_[View the full topic](https://discuss.ocaml.org/t/detecting-identity-functions-in-flambda/8180)._