История изменений

По-моему, всё, приводимое ранее, и было кортежами.

Я так понимаю тебя смущает «уникальность» типа для каждого списка. Т.е. список 'a' ::: True ::: HNil будет иметь тип HList Char (HList Bool (HList [])), а список (1::Int) ::: HNil будет иметь тип HList Int (HList []).

Я в общем понимаю что это не совсем привычно. Но всё таки я могу привести пару интересных примеров. Первое это некоторый промежуточный тип между обычным списком и гетерогенным (в смысле представленном в коде который я привёл). Это список с известной на этапе компиляции длиной. выглидит например так Vect a n где a - тип элементов в коллекции, а n - число эл-тов в списке. При этом туда можно добавлять элементы, убирать элементы и длина остаётся известной на этапе компиляции (ну т.е. если мы убрали один эл-т, то длина уменьшилась, стал тип Vect a (n-1), если прибавили, то длина увеличилась - Vect a (n+1)). Ну при этом есть дополнительная гарантия, а именно что мы никогда не вызовем head на пустом списке (пока фильтровать не начнём, конечно.. но это детали:) ).

Если следовать твоей логике то это кортеж или не кортеж? В пользу того что это кортеж говорит что тип меняется при добавлении/удалении эл-та, т.е. как у кортежа. А в пользу того что список - то что тип эл-тов один и тот же. И можно легко определить обычные для списков операции.

Сразу скажу не встречал чтобы кто то окрестил такую конструкцию кортежем. Т.е. можно конечно наверное, но смысла мало.

Следующий пример чуть более непонятный: в языках с зависимыми типами очень многие типы уникальны в том смысле что прямо зависят от значений. Т.е. там «уникальность» типов в этом смысле гораздо более заметна чем например в хаскеле. Приведу пример: функия число аргументов (а значит и тип) которой зависят от первого аргумента:

adder 0 : Int -> Int
adder 1 : Int -> Int -> Int
adder 2 : Int -> Int -> Int -> Int

По-моему, всё, приводимое ранее, и было кортежами.

Я так понимаю тебя смущает «уникальность» типа для каждого списка. Т.е. список 'a' ::: True ::: HNil будет иметь тип HList Char (HList Bool (HList [])), а список (1::Int) ::: HNil будет иметь тип HList Int (HList []).

Я в общем понимаю что это не совсем привычно. Но всё таки я могу привести пару интересных примеров. Первое это некоторый промежуточный тип между обычным списком и гетерогенным (в смысле представленном в коде который я привёл). Это список с известной на этапе компиляции длиной. выглидит например так Vect a n где a - тип элементов в коллекции, а n - число эл-тов в списке. При этом туда можно добавлять элементы, убирать элементы и длина остаётся известной на этапе компиляции (ну т.е. если мы убрали один эл-т, то длина уменьшилась, стал тип Vect a (n-1), если прибавили, то длина увеличилась - Vect a (n+1)). Ну при этом есть дополнительная гарантия, а именно что мы никогда не вызовем head на пустом списке (пока фильтровать не начнём, конечно.. но это детали:) ).

Если следовать твоей логике то это кортеж или не кортеж? В пользу того что это кортеж говорит что тип меняется при добавлении/удалении эл-та, т.е. как у кортежа. А в пользу того что список - то что тип эл-тов один и тот же. И можно легко определить обычные для списков операции.

Сразу скажу не встречал чтобы кто то окрестил такую конструкцию кортежем. Т.е. можно конечно наверное, но смысла мало.

Следующий пример чуть более непонятный: в языках с зависимыми типами очень многие типы уникальны в том смысле что прямо зависят от значений. Типы прямо зависят от значений, т.е. например Т.е. там «уникальность» типов в этом смысле гораздо более заметна чем например в хаскеле. Приведу пример: функия число аргументов (а значит и тип) которой зависят от первого аргумента:

adder 0 : Int -> Int
adder 1 : Int -> Int -> Int
adder 2 : Int -> Int -> Int -> Int