Is there a term for pure functions with only one possible implementation?

Question

I'm thinking of functions like the identity function:

val f : 'a -> 'a
let f x = x

the composition function:

val compose : ('b -> 'c) -> ('a -> 'b) -> ('a -> 'c)
let compose f g x = f (g x)

or the applicative map function if the monadic return and bind functions are defined:

val return : 'a -> 'a t
val ( >>= ) : 'a t -> ('a -> 'b t) -> 'b t

val ( >>| ) : 'a t -> ('a -> 'b) -> 'b t
let ( >>| ) t f = t >>= fun x -> f x |> return

In each of these cases, there is exactly one pure function (ignoring equivalent representations of the same logic) that could be written to satisfy the function's type signature.

Is there a term for functions like this? And why is it that there can only be one implementation?

What's your definition of "equivalent representation"? Wouldn't any correct implementation of a pure function be equivalent to any other implementation then? — glennsl, Apr 13 '19 at 17:14
You'll want to have a look at *theorems for free*, see [these introductions](https://stackoverflow.com/q/12421085/1048572). I don't know whether there is a term for this kind of functions, though. — Bergi, Apr 13 '19 at 17:15
@glennsl I mean in the sense of equivalent rewrites (using `|>` instead of parens, storing a value in a temporary variable, etc.). I think what I'm looking for is unique implementations based on type signatures. As a counterexample, the functions `val hd : 'a list -> 'a option` and `val tl : 'a list -> 'a option` are both pure functions, but this demonstrates that the type signature `'a list -> 'a option` has two valid implementations with different results, so this would not be an example of a signature I'm looking for. — Kevin Ji, Apr 13 '19 at 17:20
@Bergi Thanks for the reference; I think I was looking for some combination of parametricity / free theorems. Is there some free theorem from parametricity that could derive e.g. the existence of a unique `compose` function? If you post that as an answer I'm happy to accept that. — Kevin Ji, Apr 14 '19 at 03:41
Note that parametricity results only hold in a pure language, not if you can have side effects like state, I/O, exceptions, non-termination. E.g., in Ocaml, these are other functions of type `'a -> 'a`: `let f1 x = print "boo"; x`; `let f2 x = raise E`; `let rec f3 x = f3 x` — Andreas Rossberg, Apr 14 '19 at 05:29
@AndreasRossberg Sure, I clarified that I'm looking for pure functions. — Kevin Ji, Apr 14 '19 at 15:29

ivg · Answer 1 · 2019-04-15T15:49:47.237

You can define your own theory of functions, where the abovementioned functions will have some special semantics,

type _ fn =
  | Ident : ('a -> 'a) fn
  | Compose : (('b -> 'c) fn -> ('a -> 'b) fn -> ('a -> 'c)) fn
  | Map : (('b -> 'c) fn -> ('a -> ('a -> 'c) -> 'c) fn -> ('a -> ('a -> 'b) -> 'c)) fn
  | Gen : 'a -> 'a fn

The minimal semantics would be the reification of those abstractions into OCaml functions, i.e., the application function,

let rec app : type s. s fn -> s = function
  | Ident -> fun x -> x
  | Compose -> fun f g x -> app f (app g x)
  | Map -> fun ret bind x f -> app bind x (fun x -> app ret (f x))
  | Gen f -> f

Note, that the provided app function is stupid, as it is not using the knowledge of the functions semantics in Compose and Map applications, i.e., that Map Ident Ident is Ident,Compose Ident x is x, and many other identities which could be inferred from even such simple theory. This all is left as an exercise for the reader :)

Of course, this extra layer of indirection will be noticeable, as you can't write direct Ident x, but have to write app Ident x instead. As well as lift all regular functions into your theory, e.g.,

let 7 = app (Gen (+)) 3 4.

Is there a term for pure functions with only one possible implementation?

1 Answers1