deniok: (lambda cube)
Тут вопрос возник (не в первый раз):
typeof λx.x x
Отвечаем, например, так
> :set -XRankNTypes
> let f = (\x -> x x) :: (forall a. a -> a) -> (forall a. a -> a)
> f id 42
42
Или так
> let f' = (\x -> x x) :: (forall a. a) -> (forall a. a)
> f' undefined
*** Exception: Prelude.undefined


deniok: (lambda cube)
 
В современной теории типов выделяют два основных класса равенств: Definitional equality и Propositional equality. 
 
Ого! Ну-ка, ну-ка... )
deniok: (typed lambda)
Обогатил ру-Википедию стать ей про это дело. Ловите. Надо бы ещё, конечно, понаписать про точное определение и всякие свойства, но пока лень.

UPD: Понаписал про формальности.

UPD2: Добавил типизацию по Карри с классическим примером, демонстрирующим, что System F богаче просто-типа-лямбды. И готовящим читателя к рассуждениям про импредикативность и ограниченные версии System F.

UPD3: Уф. Доделал-таки.

deniok: (Default)
От теории множеств к теории типов. Хорошая вводная статья Майка Шульмана о том, почему именно теорию типов стоит положить в основания математики. Ну немножко философского характера, конечно, но тематика обязывает. Настоятельно рекомендую, спасибо [livejournal.com profile] alexey_rom за ссылку.

deniok: (Default)
Сделал в ру-Википедии статью про сабж. Еле поспел к Рождеству.  Держите.
deniok: (ухмыляюсь)
по расширению руВикипедии. По расширению - потому что то, что там уже есть, в половине случаев проще переписать заново, чем править. Держите, вобщем, улучшайте, исправляйте, etc:

Соответствие Карри - Говарда
deniok: (Default)
Митчелл, Основания языков программирования, перевод под ред. Н.Н.Непейводы.

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

5.2.1. Домены (domain). Переведено как области.

8.3.3. Конфлюэнтность (confluence). Переведено как сходимость.

9.4. Экзистенциальные типы (existential types). Переведено как объёмные типы (видимо перепутано с extensional, термин extensionality действительно присутствует, скажем в 8.2.5).

В целом качество перевода кажется мне довольно посредственным. Несколько раз, чтобы понять о чём речь, мне приходилось заглядывать в англоязычный оригинал.
deniok: (lambda cube)
Очень хорошие лекционные заметки Femke van Raamsdonk'а из Vrije Universiteit Amsterdam. Курс похож на тот, что я читал в CS Club'е при ПОМИ, но с несколько большим уклоном в логику и примерами с использованием Coq.
Рекомендую своим студентам как полезное дополнительное чтение и удобное введение в Coq.
deniok: (typed lambda)
Хорошая задачка из Herman Geuvers, Introduction to Type Theory (упражнение 3.17):

Построить лямбда-терм с типом ((α → β) → α) → (α → α → β) → β.

Ответы скринить не буду.

UPD: Имеется в виду просто типизированная лямбда. То есть fix и прочие Y-комбинаторы нам недоступны.

UPD2: Рекурсия ни в каком виде недоступна!
deniok: (typed lambda)
Отталкиваясь от полученной в прошлом посту просьбы, попытаюсь рассказать о Σ-типах.

deniok: (typed lambda)
Для чего нужна Π-абстракция при наличии зависимых типов?

А вот для чего... )
deniok: (Default)
В 1997 небезызвестные Simon Peyton Jones и Erik Meijer предложили промежуточный внутри-компиляторный богато-типизированный язык Henk. Сегодня я понял причину, почему язык так назван. Механизм - тот же, что и в Хаскелле.

Henk Barendregt - голландский логик,  изобретатель лямбда-куба (1991), автор штудируемого мною нынче Lambda Calculi with Types. "Восхищайтесь" (с)[profile] thesz
deniok: (Default)
О сколько нам открытий чудных дарит изучение просто типизированной чистой лямбды.

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

Сохраняется ли при этом тип? То есть верно ли утверждение

(Двойная стрелочка читается "бета-редуцируемо к")

Ответ под катом... )

Profile

deniok: (Default)
deniok

April 2017

S M T W T F S
      1
23 45678
9101112131415
16171819202122
23242526272829
30      

Syndicate

RSS Atom

Style Credit

Expand Cut Tags

No cut tags
Page generated Sep. 24th, 2017 03:17 am
Powered by Dreamwidth Studios