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

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

Для кого-то это может быть очевидно, но для меня это, черт возьми, не очевидно.


person hao ramirez    schedule 14.08.2016    source источник


Ответы (2)


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

Для Сводка по тегу SO «зависимый-тип»: «Зависимые типы типы, зависящие от ценностей ". Perl 6 поддерживает типы, зависящие от значений, вот и все.

Для Обзор изменений, внесенных Awwaiid, которые добавили Perl 6 на страницу Википедии на Dependent Типы говорят: «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 генерирует зависимые типы? Возможно, это то, о чем думает Авваид.

person raiph    schedule 15.08.2016
comment
Что ж, в том смысле, что perl 6 имеет типы, зависящие от значений, тогда да, конечно. По этому определению C тоже. Но наличие только индексированных типов само по себе не очень полезно. - person Ven; 31.07.2017
comment
FWIW, Я также рассматривал возможность взлома параметризованных ролей, но только count версия работает (что развязывает их во время выполнения). Для ролей потребуется фаза создания экземпляров (например, шаблонов C ++), чтобы получить что-то вроде зависимых типов, но этого нет в меню :-). - person Ven; 31.07.2017

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

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

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;
person Christoph    schedule 16.08.2016
comment
Я согласен с общим мнением, хотя хардкор-зависимый машинист (или любой другой, называемый сторонниками зависимых типов) может возразить, что тип не проверяется во время компиляции, и поэтому ваш пример не учитывается. Думаю, все зависит от интерпретации. - person moritz; 24.07.2017
comment
Что сказал @moritz. Среда выполнения не типизирована, поэтому она должна выполняться во время компиляции. - person Ven; 31.07.2017