AZ
хотя если писать функцию Type -> Type -> foo то тогда да
foo: a -> a
foo: Vect n elem -> Vect n elem2
Size: a a a
2020 August 13
p
первый это генерики в обычном понимании, второй это n - завтип
AZ
foo: a -> a
foo: Vect n elem -> Vect n elem2
foo: Vect n elem -> Vect n elem2
у тебя тут неявно генерики используются лол
p
разницу семантическую видишь? я нет
AZ
в одном случае есть генерик параметр a, а в другом - n
AZ
но ты прав
AZ
по крайней мере в идрисе это действительно так
p
по крайней мере в идрисе это действительно так
да!
AZ
ведь генерик это функция типа Type -> Type
AZ
то есть просто тайплевел функа
p
на самом деле можно свою систему типов построить
p
потому что в идрисе она построена как раз снаружи
AZ
блин как мне в шарпе не хватает завтипов
SP
минвайл в руби добавили паттерн матчинг и жит еще в 2019. но типы не завезли
AZ
ну или хотя бы адт
AZ
но с завтипами гибче
p
блин как мне в шарпе не хватает завтипов
да похуй на завтипы, дайте хотя бы АДТ и тайпклассы
Ct
Хм, а может кто объяснить из чего компилятор делает вывод, что "data from
name is returned here"?p
и да, завтипов в расте не будет никогда по понятным причинам