0
ответов
Какие типы и / или термины в system-f не могут быть выражены в Hindley Milner
Я помню, как где-то читал, что Hindley Milner был ограничением для system-f. Если это так, не мог бы кто-нибудь предоставить мне некоторые термины, которые можно ввести в system-f, но не в HM.
вопрос задан: 1 March 2012 12:09
0
ответов
Выражение лямбда-исчисления, реализующее применение функции
Я только что нашел следующее выражение лямбда-исчисления: (((λ f . (λ x . (f x)))) (λ a . a)) (λ b . b)) То есть это функция, которая принимает аргумент f и возвращает другую функцию, которая принимает аргумент ...
вопрос задан: 1 February 2012 11:01
0
ответов
Встраивание более высоких типов (монад!) В нетипизированное лямбда-исчисление
В нетипизированном лямбда-исчислении можно кодировать различные типы с помощью функций более высокого порядка. Примеры:
ноль = λfx. Икс
один = λfx. FX
два = λfx. f (fx)
три = λfx. f (f (fx))
и т.д ...
вопрос задан: 20 January 2012 01:20
0
ответов
Что такое «свободная переменная»?
(Я уверен, что на этот сайт уже, должно быть, уже был дан ответ, но поиск наводнен концепцией вызова free () для переменной в C.) Я пришел через термин "сокращение eta", который был ...
вопрос задан: 13 January 2012 20:49
0
ответов
что это за уравнение с лямбда-обозначением «m >> n = m >> = \ _ -> n» в объявлении монады?
class Monad m where return :: a -> ma (>> =) :: ma -> (a -> mb) -> mb (>>) :: ma -> mb -> mbm >> n = m >> = \ _ -> n fail :: String - & ...
вопрос задан: 31 December 2011 19:50
0
ответов
лямбда-исчисление: передача двух значений в один параметр без каррирования
Я не могу понять, почему в нетипизированном лямбда-исчислении разрешено следующее бета-сокращение: (λx.xy) (uv ) -> ((uv) y) В частности, я не могу понять, как можно передать два параметра u и v ...
вопрос задан: 7 December 2011 14:38
0
ответов
Код, реализующий уникальные возможности каждого ребра лямбда-исчисления
Я не могу объяснить термин лямбда-куб намного лучше, чем это делает Википедия: [...] λ-куб - это основа для исследования осей уточнения в исчислении построений Кокванда , начиная с ...
вопрос задан: 27 November 2011 02:57
0
ответов
Что лямбда-исчисление говорит о возвращаемых значениях?
К настоящему времени хорошо известна теорема лямбда-исчисления, что любая функция, принимающая два или более аргумента, может быть записана посредством каррирования в виде цепочки функций, принимающих один Аргумент: # Псевдокод для ...
вопрос задан: 22 November 2011 14:22
0
ответов
Y-комбинатор в D?
Я пытаюсь лучше изучить Y-комбинатор (я вроде как понимаю его на схеме) и реализовать его в D 2.0, и я с треском проваливается: auto fact = delegate (uint delegate (uint) recurse)
{...
вопрос задан: 4 August 2011 15:51
0
ответов
Вычитание церковных цифр в haskell
Я пытаюсь реализовать церковные цифры в Haskell, но у меня возникла небольшая проблема. Haskell жалуется на бесконечный тип с проверкой Occurs: не удается построить бесконечный тип: t = (t -> t1) -> (...
вопрос задан: 6 July 2011 11:38
0
ответов
Церковные цифры в haskell
Я пытаюсь напечатать церковные цифры в haskell, используя определения: 0: = λfx.x
1: = λfx.f x Код Haskell: c0 = \ f x -> x
c1 = \ fx -> fx Когда я ввожу его в консоль haskell, я получаю ...
вопрос задан: 24 June 2011 02:37
0
ответов
Call by value in the lambda calculus
I'm working my way through Types and Programming Languages, а Пирс, для стратегии call by value reduction, приводит пример термина id (id (λz. id z)). Внутренний редекс id (λz. id z) ...
вопрос задан: 29 May 2011 18:43
0
ответов
Что означает eta reduce в контексте HLint
Я просматриваю учебник http: // haskell .org / haskellwiki / How_to_write_a_Haskell_program import System.Environment main :: IO ()
main = getArgs >> = печать. haqify. head haqify s = "Haq!" ++ ...
вопрос задан: 26 April 2011 22:39
0
ответов
Y Combinator в схеме с помощью Define
Чтобы узнать, что такое комбинатор с фиксированной точкой и для чего он используется, я написал свой собственный. Но вместо того, чтобы писать его со строго анонимными функциями, как в примере из Википедии, я просто использовал define: (define ...
вопрос задан: 14 January 2011 03:06
0
ответов
Стратегия удаления сахара в Haskell
Я разрабатываю виртуальную машину для чисто функциональных программ, и я хотел бы иметь возможность тестировать и использовать широкий спектр уже доступных модулей Haskell. Виртуальная машина принимает в качестве входных данных ...
вопрос задан: 29 December 2010 02:24
0
ответов
Как бы вы реализовали функцию бета-сокращения в F #?
Я пишу лямбда-исчисление в F #, но я застрял на реализации бета-редукции (замена формальных параметров фактическими параметрами). (лямбда xe) f
-> e [f / x] пример использования: (...
вопрос задан: 30 October 2010 15:06
0
ответов
Ввод комбинатора Y
http://muaddibspace.blogspot.com/2008/01/type-inference-for-simply-typed-lambda.html - это краткое определение просто набранное лямбда-исчисление в Прологе. Выглядит нормально, но затем он заявляет, что ...
вопрос задан: 13 September 2010 17:28
0
ответов
Практическое применение расчета SKI и BCKW
Я могу понять, как создавать и думать о расчетах SKI и BCKW, но никогда не могу найти практическое применение. Может я недостаточно глубоко смотрю? То есть, мне интересно, если (только пример ...
вопрос задан: 11 September 2010 00:58