Представление функций как типов

Question

Функция может быть сильно вложенной структурой:

function a(x) {
  return b(c(x), d(e(f(x), g())))
}

Во-первых, интересно, есть ли у функции экземпляр. То есть оценка функции является экземпляром функции. В этом смысле тип - это функция, а экземпляр - ее оценка. Если это возможно, то как моделировать функцию как тип (в некотором языке, ориентированном на теорию типов, например, на Haskell или Coq).

Это почти как:

type a {
  field: x
  constructor b {
    constructor c {
      parameter: x
    },
    ...
  }
}

Но я не уверен, что я не на правильном пути. Я знаю, что вы можете сказать, что функция имеет тип [return]. Но мне интересно, можно ли считать функцию типом, и если да, то как моделировать ее как тип на языке, ориентированном на теорию типов, где она моделирует фактическую реализацию функции.

Answer 1

Я думаю, что проблема в том, что типы, основанные непосредственно на реализации (давайте назовем их "i-типы"), не кажутся очень полезными, и у нас уже есть хорошие способы их моделирования (так называемые "программы" - ха-ха).

В вашем конкретном примере полный i-тип вашей функции, а именно:

type a {
  field: x
  constructor b {
    constructor c {
      parameter: x
    },
    constructor d {
      constructor e { 
        constructor f { 
          parameter: x 
        } 
        constructor g {
        }
    }
  }
}

это просто многословный, альтернативный синтаксис для самой реализации. Таким образом, мы могли бы написать этот i-тип (в синтаксисе, подобном Haskell) как:

itype a :: a x = b (c x) (d (e (f x) g))

С другой стороны, мы могли бы напрямую преобразовать реализацию вашей функции в синтаксис уровня терминов Haskell, чтобы записать ее как:

a x = b (c x) (d (e (f x) g))

и i-тип и реализация - это одно и то же.

Как бы вы использовали эти i-типы? Компилятор может использовать их, получая аргументы и возвращаемые типы для проверки типов программы. (К счастью, существуют хорошо известные алгоритмы, такие как Алгоритм W, для одновременного получения и проверки типов аргументов и возвращаемых типов из i-типов этого типа.) Программисты, вероятно, не будут использовать i-типы напрямую - они слишком сложный в использовании для рефакторинга или рассуждений о поведении программы. Возможно, они захотят взглянуть на типы, полученные компилятором, для аргументов и возвращаемого типа.

В частности, "моделирование" этих i-типов на уровне типов в Haskell не кажется продуктивным. Haskell уже может моделировать их на уровне термина. Просто напишите свои i-types как программу на Haskell:

a x = b (c x) (d (e (f x) g))
b s t = sqrt $ fromIntegral $ length (s ++ t)
c = show
d = reverse
e c ds = show (sum ds + fromIntegral (ord c))
f n = if even n then 'E' else 'O'
g = [1.5..5.5]

и не запускай его. Поздравляем, вы успешно смоделировали эти i-типы! Вы даже можете использовать GHCi для запроса производного аргумента и возвращаемых типов:

> :t a
a :: Floating a => Integer -> a   -- "a" takes an Integer and returns a float
>

Теперь вы, возможно, представляете, что существуют ситуации, когда реализация и i-тип расходятся, возможно, когда вы начинаете вводить буквальные значения. Например, может быть, вы чувствуете, как функция f выше:

f n = if even n then 'E' else 'O'

должен быть назначен тип что-то вроде следующего, который не зависит от конкретных литеральных значений:

type f {
  field: n
  if_then_else {
    constructor even {    -- predicate
      parameter: n
    }
    literal Char          -- then-branch
    literal Char          -- else-branch
}

Опять же, тем не менее, вы бы лучше определить произвольный уровень терминов Char, лайк:

someChar :: Char
someChar = undefined

и моделирование этого i-типа на уровне терминов:

f n = if even n then someChar else someChar

Опять же, до тех пор, пока вы не запустите программу, вы успешно смоделировали i-тип f, может запрашивать его аргумент и возвращать типы, проверять тип как часть большой программы и т. д.

Answer 2

Я не совсем понимаю, к чему вы стремитесь, поэтому я постараюсь указать на некоторые связанные термины, о которых вы, возможно, захотите прочитать.

Функция имеет не только возвращаемый тип, но и тип, который описывает ее аргументы. Так что (Хаскель) тип f гласит: "f принимает Int и Float и возвращает список с плавающей точкой".

f :: Int -> Float -> [Float]
f i x = replicate i x

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

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

Возвращаясь к первой части вашего вопроса, Beta Reduction - это процесс заполнения конкретных значений для каждого из аргументов функции. Я слышал, что люди описывают выражения как "после сокращения" или "полностью сокращенные", чтобы подчеркнуть некоторую стадию в этом процессе. Это похоже на функцию вызова сайта, но подчеркивает выражение и аргументы, а не окружающий контекст.