Поддерживает ли Perl6 зависимые типы?

Question

Недавно я просматривал страницу википедии о зависимых типах, и мне было интересно; Perl 6 действительно вводит зависимые типы? Я не могу найти надежный источник, утверждающий это.

Это может быть очевидным для некоторых, но это, конечно же, чертовски не очевидно для меня.

Answer 1

Против Ven, в комментариях после ответа Perl 6 на вопрос SO "Есть ли язык с ограничиваемыми типами?", Он написал "perl6 не имеет зависимых типов", а позже написал "зависимый тип, вероятно, нет,... хорошо, если мы получим разрешимый where s... "в обмене на # perl6. (Ответ Ларри Уолла был " что вызывает несколько проблем у друзей ". Кстати, безусловно, лучший способ получить авторитетный ответ на все вопросы Perl 6 - это спросить TimToady через # Perl6.)

Итогом для тега SO "зависимый тип" является "Зависимые типы - это типы, которые зависят от значений". Perl 6 поддерживает типы, которые зависят от значений, так что есть что.

В сводке редактирования изменения Awwaiid, добавившего Perl 6 на страницу Википедии о зависимых типах, написано: "Perl 6... имеет неразрешимые зависимые типы".

Страница Википедии начинается с:

зависимый тип - это тип, определение которого зависит от значения. "Пара целых чисел" - это тип. "Пара целых чисел, где второе больше первого" является зависимым типом из-за зависимости от значения.

Вот один из способов создать тип по этим направлениям в Perl 6:

subset LessMorePair of Pair where { $_.key < $_.value }
subset MoreLessPair of Pair where { $_.key > $_.value }

multi sub foo (        Pair) { "  P" }
multi sub foo (LessMorePair) { "LMP" }
multi sub foo (MoreLessPair) { "MLP" }

for 1 => 1, 1 => 2, 2 => 1 { say foo $_ }

#   P
# LMP
# MLP

Означает ли это Perl 6 subset функция генерирует зависимые типы? Возможно, именно об этом думает Awwaiid.

Answer 2

Возможно, да, поскольку подмножества являются типами, которые могут зависеть от произвольных условий. Однако система типов будет классифицироваться как несостоятельная, так как инварианты типов не применяются.

В частности, ограничение типа переменной проверяется только при присваивании, поэтому модификации объекта, которые делают его отбрасываемым из подмножества, приведут к тому, что переменная будет содержать объект, которого она не должна иметь, например

subset OrderedList of List where [<=] @$_;

my OrderedList $list = [1, 2, 3];
$list[0] = 42;
say $list ~~ OrderedList;

Вы можете использовать некоторые мета-объектные мастера, чтобы заставить объектную систему автоматически проверять тип после любого вызова метода, помещая объекты в прозрачные защитные объекты.

Наивная реализация может выглядеть так:

class GuardHOW {
    has $.obj;
    has $.guard;
    has %!cache =
        gist => sub (Mu \this) {
            this.DEFINITE
                ?? $!obj.gist
                !! "({ self.name(this) })";
        },
        UNBOX => sub (Mu $) { $!obj };

    method find_method(Mu $, $name) {
        %!cache{$name} //= sub (Mu $, |args) {
            POST $!obj ~~ $!guard;
            $!obj."$name"(|args);
        }
    }

    method name(Mu $) { "Guard[{ $!obj.^name }]" }
    method type_check(Mu $, $type) { $!obj ~~ $type }
}

sub guard($obj, $guard) {
    use nqp;
    PRE $obj ~~ $guard;
    nqp::create(nqp::newtype(GuardHOW.new(:$obj, :$guard), 'P6int'));
}

Это приведет к следующей ошибке:

my $guarded-list = guard([1, 2, 3], OrderedList);
$guarded-list[0] = 42;