Есть ли термин для чистых функций только с одной возможной реализацией? - PullRequest
Новая
       14

Есть ли термин для чистых функций только с одной возможной реализацией?

0 голосов
/ 13 апреля 2019

Я имею в виду такие функции, как функция идентификации: 

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

функция композиции: 

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

или аппликативная функция map, если монадическая return иbind определены функции: 

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

В каждом из этих случаев есть ровно одна чистая функция (игнорирующая эквивалентные представления одной и той же логики), которая может быть написана для удовлетворения сигнатуры типа функции.

Есть ли термин для таких функций?И почему может быть только одна реализация?

1 Ответ

0 голосов
/ 15 апреля 2019

Вы можете определить свою собственную теорию функций, в которой вышеупомянутые функции будут иметь особую семантику, 

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

Минимальной семантикой было бы преобразование этих абстракций в функции OCaml, то есть функцию приложения, 

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

Обратите внимание, что предоставленная функция app является глупой, поскольку она не использует знание семантики функций в приложениях Compose и Map, т. Е. Что Map Ident Ident равно Ident, Compose Ident x x и многие другие тождества, которые можно вывести из такой простой теории. Все это оставлено читателю в качестве упражнения :)

Конечно, этот дополнительный уровень косвенности будет заметен, так как вы не можете написать прямое Ident x, но вместо этого вы должны написать app Ident x. А также поднять все регулярные функции в вашу теорию, например, 

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