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

Question

Я недавно смотрел на wikipedia page for dependent types, и мне было интересно; действительно ли Perl 6 действительно вводит зависимые типы? Я не могу найти надежного источника, утверждающего это.

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

Answer 1

против Вен, в комментариях после ответа Perl 6 на вопрос SO «Есть ли язык с constrainable типов?», Пишет "perl6 doesn't have dependant types" и позже написал «зависимый тип, вероятно, не ... ну, если мы получим разрешимый where s ... "в обмен на # perl6. (Ответ Ларри Уолла был "what's a few halting problems among friends". Кстати, на сегодняшний день является лучшим способом, чтобы получить достоверный ответ на все вещи, Perl 6, чтобы спросить TimToady через # Perl6.)

Для резюме для 'dependent-type' SO tag является «Зависимые типы типы, которые зависят от значений ». Perl 6 поддерживает типы, зависящие от значений, поэтому есть это.

Для резюме редактирования для изменения по Awwaiid, который добавил Perl 6 на страницу Википедии на Dependent Types говорит «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 

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

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;