Описание тега system-f
1
ответ
Невозможно понять термин F-омега
Я читаю статью о Fω и не могу понять причины этого утверждения: Типовой член типа (∀γ:*. F γ → β) показывает, что F - постоянная функция, которая всегда возвращает β. Я предполагаю, что "F γ → β" - это термин типа, т. Е. Тип стрелки. Этот тип стрелк…
29 ноя '17 в 10:19
3
ответа
Что требуется для того, чтобы расширить реализацию нетипизированного лямбда-исчисления, чтобы охватить просто типизированное лямбда-исчисление?
Мэтт Майт говорит о реализации интерпретатора лямбда-исчисления в 7 строках схемы: ; eval takes an expression and an environment to a value (define (eval e env) (cond ((symbol? e) (cadr (assq e env))) ((eq? (car e) 'λ) (cons e env)) (else (apply (e…
21 июн '16 в 05:14
1
ответ
Полиморфное самостоятельное применение
У меня есть пример системного плиморфизма F, который я не совсем понимаю: Если бы я удалил типы, он бы остался: \f.\ Af (f a), который не имеет смысла. ты можешь помочь мне с этим? Спасибо!
08 фев '16 в 05:33
1
ответ
Как Haskell добавил полноту по Тьюрингу в System F?
Я читал о различных системах типов и лямбда-исчислениях и вижу, что все типизированные лямбда-исчисления в лямбда-кубе сильно нормализуются, а не эквивалентны по Тьюрингу. Это включает Систему F, простейшее лямбда-исчисление плюс полиморфизм. Это пр…
12 авг '14 в 02:49
1
ответ
В чем разница между этими полиморфными типами?
В системе F, в чем разница между следующими 3 типами: Воспроизводится в тексте здесь: ∀X.((X → X) → (X → X)) ∀X.((X → X) → ∀X.(X → X)) ((∀X.X → X) → (∀X.X → X)) Второй является более общим, чем первый?
08 фев '16 в 15:00
2
ответа
Типовая абстракция в GHC Haskell
Я хотел бы получить следующий пример для проверки типа: {-# LANGUAGE AllowAmbiguousTypes #-} {-# LANGUAGE RankNTypes #-} {-# LANGUAGE TypeApplications #-} {-# LANGUAGE TypeFamilies #-} module Foo where f :: Int -> (forall f. Functor f => Secre…
03 май '18 в 15:59
1
ответ
Оператор связывания Haskell в системе F, включая виды
Мне нужно знать, что такое тип System F оператора связывания типа Haskell (>>=). До сих пор я писал это так: (M::*->* A::*) -> (A::* -> (M::*->* B::*)) -> (M::*->* B:*) Это правильно? Если это правильно, как мне найти окончательный…
08 фев '16 в 21:04
1
ответ
Как систематически подсчитать количество жителей данного типа?
Как систематически вычислить количество жителей данного типа в Системе F? Предполагая следующие ограничения: Все жители кончаются, т.е. нет дна. У всех жителей отсутствуют побочные эффекты. Например (с использованием синтаксиса Haskell): Bool имеет …
18 окт '15 в 12:58
0
ответов
Кодирование универсальных типов в терминах экзистенциальных типов?
В системе F тип exists a. P может быть закодирован как forall b. (forall a. P -> b) -> b в том смысле, что любой термин System F, использующий экзистенциал, может быть выражен в терминах этого кодирования с соблюдением правил типирования и сок…
19 ноя '18 в 13:33
1
ответ
"Недопустимый полиморфный или квалифицированный тип" в объявлении экземпляра (деревья стиля System-F)
Я экспериментирую с реализацией структур данных в стиле System-F в Haskell. Я буду использовать A <B> означать применение термина A к типу B просто, чтобы сделать это однозначным (также используя заглавные буквы для типов). Скажем Tree <T&g…
23 ноя '15 в 19:42
0
ответов
Система кодирования неисправностей омега в финале tagless в idris
Поэтому я пытаюсь сделать систему омега в окончательном стиле без тегов. Я успешно закодировал систему f, как показано в следующем коде (также приведен некоторый пример)(также, пожалуйста, не обращайте внимания на тот факт, что логический вывод не р…
05 июл '18 в 01:22
2
ответа
Пример типа в Системе F, который недоступен в выводе типа Хиндли Милнера
В разделе "Что такое Хиндли Милнер" говорится: Хиндли-Милнер - это ограничение System F, которое допускает больше типов, но требует от программиста аннотаций. У меня вопрос: что является примером типа, доступного в системе F, который недоступен в Hi…
02 июн '14 в 13:28
1
ответ
Моделирование параметрического полиморфизма системы F при множестве
В Системе F тип полиморфного типа * (поскольку это единственный тип в System F в любом случае...), например, для следующего закрытого типа: [] ⊢ (forall α : *. α → α) : * Я хотел бы представлять System F в Агде, и потому что все в *, Я думал, что я …
23 ноя '15 в 03:22
1
ответ
Хаскелл не хочет набирать полиморфизм высокого ранга
Я не понимаю, почему эта программа не печатается: type Test a = forall z. (a -> z) -> z cons :: a -> Test a cons = \a -> \p -> p a type Identity = forall x. x -> x t :: Identity t = \x -> x c :: Test Identity c = cons (t :: Iden…
24 ноя '14 в 16:18
1
ответ
Какова каноническая реализация Системы F?
Система F - отличный способ просто рассуждать о типах при программировании прототипа. Помимо реализации этого, я бы хотел использовать существующую реализацию. При поиске реализаций, кажется, их нет - и я не уверен почему. Мой вопрос: какова канони…
25 июн '16 в 02:38
1
ответ
Функция Zip в системе F
Определим тип списка list = forall 'a, 'x. ('a -> 'x -> 'x) -> 'x -> 'x где например nil = Λ'a . Λ'x . λ(c : 'a -> 'x -> 'x) . λ(e : 'x) . e cons = Λ'a . Λ'x . λ(head : 'a) . λ(tail : list 'a 'x) . λ(c : 'a -> 'x -> 'x) . λ(e…
25 май '19 в 23:25
1
ответ
Система F Церковные цифры в Агде
Я хотел бы протестировать некоторые определения в системе F, используя Agda в качестве моего средства проверки типов и оценщика. Моя первая попытка ввести церковные натуральные числа была написана Num = forall {x} -> (x -> x) -> (x -> x)…
06 июн '19 в 16:55
1
ответ
Может ли тип статически гарантировать, что функция для пар лишь частично зависит от его ввода?
Рассмотрим тип функции от 's к парам b'песок cs,. (Я буду использовать нотацию Haskell для типов и функций, но это не вопрос самого Haskell.) Есть много таких функций, в том числе те, в которых оба, один или ни один из (b, c) выходы зависят от. Пред…
23 июл '21 в 01:40
1
ответ
Характеризуя тип функций, которые могут принимать `()` в качестве входных данных (без мономорфизации)
Вот несколько простых функций: f1 :: () -> () f1 () = () f2 :: a -> a f2 a = a f3 :: a -> (a, a) f3 a = (a, a) f4 :: (a, b) -> a f4 (a, b) = a Все, и могут принимать в качестве входных данных. С другой стороны, конечно, f4 не могу принят…
27 июл '21 в 23:27