Пошел за старыми статьями Вадлера...

[thesz]

...наткнулся на новые.

Очень интересно про линейную логику (которая Linear logic):Two different operational interpretations of intuitionistic linear logic have been proposed in the literature. The simplest interpretation recomputes non-linear values every time they are required. It has good memory-management properties, but is often dismissed as

Comments

[deni_ok]

Название одной из статей понравилось:
Once upon a type.
:)

[thesz]

Да, Вадлер славен названиями статей. ;)

[nealar]

Не догоняю. Логика - это такая система вывода. Причём тут recomputation?

[thesz]

Логика - это такая система отслеживания инвариантов над вычислениями.

Помнишь про Curry-Howard isomorphism? ;)

[nealar]

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

[thesz]

Это к автору статьи, пожалуй.

Похоже не Uniqueness

[vag_vagoff]

Система сильно напоминает Клиновский Uniqueness.

Например, программа с ошибкой уникальности

testf :: *{Int} -> (Int,*{Int})
testf a
# x = size a
y = a.[0]
= (x + y, a)

заработает, если добавить стриктнесса:

testf :: *{Int} -> (Int,*{Int})
testf a
#! x = size a
y = a.[0]
= (x + y, a)

Re: Похоже не Uniqueness

[nponeccop]

Странно не видеть при этом ссылок на работы Клиновской школы (Plasmeijer
et al)

Re: Похоже не Uniqueness

[thesz]

Так линейная логика и дала точку опоры уникальным типам Clean.

См. по той же ссылке статью Linear types can change the world.