История изменений
Исправление AndreyKl, (текущая версия) :
Матан не в типах, а в доказательстве.
Ты понимаешь, тут штука сложнее. Это две стороны одной медали.
Т.е. когда ты пишешь с зависимыми типами, ты либо ими пользуешься, но тогда ты _обязан_ работать с доказательствами (либо в стиле идриса, либо в стиле кока). Либо ты пытаешься обходится без доказательств (ну, по недостатку умения например), но тогда всё сползает к более обычным типам.
Т.е. как пример
after : (xs ys : list a) -> (length xs < length ys) -> list a
after (x::xs) (y::ys) prf = after xs ys (congr S prf)
after [] ys _ = ys
Конкретно
prf имеет тип lenght(x::xs) < length(y::ys), а (congr S prf) - это доказательство того, что если lenght(x::xs) < length(y::ys), то и length(xs) < length(ys)Соответсвенно, на следующий уровень рекурсии уже передаётся доказательство того что
length(xs) < length(ys).А в конце мы имеем «бесплатно» доказательство того что список не пуст
0 < length(ys).Но тип нашей функции не возвращает эту информацию. Хотя при вызове (другой) функции от данного списка это освободило бы нас от проверки на пустоту.
Лучше было бы как то так:
after : (xs ys : list a) -> (length xs < length ys) -> (zs : list a ** 0 < length zs)
after (x::xs) (y::ys) prf = after xs ys (congr S prf)
after [] ys prf = (ys, prf)
Но чтобы это понимать (т.е. написать тип), надо понимать как доказывать, иначе не получится ни передать во внутрь, ни вернуть.
Кстати, насчёт с++, я не зря в начале нашего с тобой разговора упомянул что в курсе что можно изобразить (хоть и гипотетически «в курсе», любопытно глянуть на практике на простой случай и как с ним работать), но на брэйнфаке тоже можно писать программы. Так это я к тому что как ты будешь на с++ со всей этой машинерией работать? Кок показывает все типы и цели и их изменения (от применения тактик), идрис тоже самое.
А что с++? Как работать там со всем этим? Я честно говоря думаю что это будет не просто боль, а адская боль (если вообще осуществимо что то сложнее хеллоуворлда). По русски говоря, не смотря на то что тебе удастся выразить зависимый тип на шаблонах для какого то простого случая (а может и для непростого ,при должных затратах труда), сделать ты всё равно с этим ничего не сможешь. Так что смысла в этом нет никакого.
Ровно поэтому аргумент этот («на си++ тоже можно..») мягко говоря слабоват.
Исправление AndreyKl, :
Матан не в типах, а в доказательстве.
Ты понимаешь, тут штука сложнее. Это две стороны одной медали.
Т.е. когда ты пишешь с зависимыми типами, ты либо ими пользуешься, но тогда ты _обязан_ работать с доказательствами (либо в стиле идриса, либо в стиле кока). Либо ты пытаешься обходится без доказательств (ну, по недостатку умения например), но тогда всё сползает к более обычным типам.
Т.е. как пример
after : (xs ys : list a) -> (length xs < length ys) -> list a
after (x::xs) (y::ys) prf = after xs ys (congr S prf)
after [] ys _ = ys
Конкретно
prf имеет тип lenght(x::xs) < length(y::ys), а (congr S prf) - это доказательство того, что если lenght(x::xs) < length(y::ys), то и length(xs) < length(ys)Соответсвенно, на следующий уровень рекурсии уже передаётся доказательство того что
length(xs) < length(ys).А в конце мы имеем «бесплатно» доказательство того что список не пуст
0 < length(ys).Но тип нашей функции не возвращает эту информацию. Хотя при вызове (другой) функции от данного списка это освободило бы нас от проверки на пустоту.
Лучше было бы как то так:
after : (xs ys : list a) -> (length xs < length ys) -> (zs : list a ** 0 < length zs)
after (x::xs) (y::ys) prf = after xs ys (congr S prf)
after [] ys prf = (ys, prf)
Но чтобы это понимать (т.е. написать тип), надо понимать как доказывать, иначе не получится ни передать во внутрь, ни вернуть.
Кстати, насчёт с++, я не зря в начале нашего с тобой разговора упомянул что в курсе что можно изобразить (хоть и гипотетически «в курсе», любопытно глянуть на практике на простой случай и как с ним работать), но на брэйнфаке тоже можно писать программы. Так это я к тому что как ты будешь на с++ со всей этой машинерией работать? Кок показывает все типы и цели и их изменения (от применения тактик), идрис тоже самое.
А что с++? Как работать там со всем этим? Я честно говоря думаю что это будет не просто боль, а адская боль (если вообще осуществимо что то сложнее хеллоуворлда). По русски говоря, не смотря на то что тебе удастся выразить зависимый тип на шаблонах для какого то простого случая (а может и для непростого ,при должных затратах труда), сделать ты всё равно с этим ничего не сможешь. Так что смысла в этом нет.
Исправление AndreyKl, :
Матан не в типах, а в доказательстве.
Ты понимаешь, тут штука сложнее. Это две стороны одной медали.
Т.е. когда ты пишешь с зависимыми типами, ты либо ими пользуешься, но тогда ты _обязан_ работать с доказательствами (либо в стиле идриса, либо в стиле кока). Либо ты пытаешься обходится без доказательств (ну, по недостатку умения например), но тогда всё сползает к более обычным типам.
Т.е. как пример
after : (xs ys : list a) -> (length xs < length ys) -> list a
after (x::xs) (y::ys) prf = after xs ys (congr S prf)
after [] ys _ = ys
Конкретно
prf имеет тип lenght(x::xs) < length(y::ys), а (congr S prf) - это доказательство того, что если lenght(x::xs) < length(y::ys), то и length(xs) < length(ys)Соответсвенно, на следующий уровень рекурсии уже передаётся доказательство того что
length(xs) < length(ys).А в конце мы имеем «бесплатно» доказательство того что список не пуст
0 < length(ys).Но тип нашей функции не возвращает эту информацию. Хотя при вызове (другой) функции от данного списка это освободило бы нас от проверки на пустоту.
Лучше было бы как то так:
after : (xs ys : list a) -> (length xs < length ys) -> (zs : list a ** 0 < length zs)
after (x::xs) (y::ys) prf = after xs ys (congr S prf)
after [] ys prf = (ys, prf)
Но чтобы это понимать (т.е. написать тип), надо понимать как доказывать, иначе не получится ни передать во внутрь, ни вернуть.
Кстати, насчёт с++, я не зря в начале нашего с тобой разговора упомянул что в курсе что можно изобразить (хоть и гипотетически «в курсе», любопытно глянуть на практике на простой случай и как с ним работать), но на брэйнфаке тоже можно писать программы. Так это я к тому что как ты будешь на с++ со всей этой машинерией работать? Кок показывает все типы и цели и их изменения (от применения тактик), идрис тоже самое.
А что с++? Как работать там со всем этим? Я честно говоря думаю что это будет не просто боль, а адская боль. По русски говоря, не смотря на то что тебе удастся выразить зависимый тип на шаблонах для какого то простого случая (а может и для непростого ,при должных затратах труда), сделать ты всё равно с этим ничего не сможешь. Так что смысла в этом нет.
Исправление AndreyKl, :
Матан не в типах, а в доказательстве.
Ты понимаешь, тут штука сложнее. Это две стороны одной медали.
Т.е. когда ты пишешь с зависимыми типами, ты либо ими пользуешься, но тогда ты _обязан_ работать с доказательствами (либо в стиле идриса, либо в стиле кока). Либо ты пытаешься обходится без доказательств (ну, по недостатку умения например), но тогда всё сползает к более обычным типам.
Т.е. как пример
after : (xs ys : list a) -> (length xs < length ys) -> list a
after (x::xs) (y::ys) prf = after xs ys (congr S prf)
after [] ys _ = ys
Конкретно
prf имеет тип lenght(x::xs) < length(y::ys), а (congr S prf) - это доказательство того, что если lenght(x::xs) < length(y::ys), то и length(xs) < length(ys)Соответсвенно, на следующий уровень рекурсии уже передаётся доказательство того что
length(xs) < length(ys).А в конце мы имеем «бесплатно» доказательство того что список не пуст
0 < length(ys).Но тип нашей функции не возвращает эту информацию. Хотя при вызове (другой) функции от данного списка это освободило бы нас от проверки на пустоту.
Лучше было бы как то так:
after : (xs ys : list a) -> (length xs < length ys) -> (zs : list a ** 0 < length zs)
after (x::xs) (y::ys) prf = after xs ys (congr S prf)
after [] ys prf = (ys, prf)
Но чтобы это понимать (т.е. написать тип), надо понимать как доказывать, иначе не получится ни передать во внутрь, ни вернуть.
Кстати, насчёт с++, я не зря в начале нашего с тобой разговора упомянул что в курсе что можно изобразить, но на брэйнфаке тоже можно писать программы. Так это я к тому что как ты будешь на с++ со всей этой машинерией работать? Кок показывает все типы и цели и их изменения (от применения тактик), идрис тоже самое.
А что с++? Как работать там со всем этим? Я честно говоря думаю что это будет не просто боль, а адская боль. По русски говоря, не смотря на то что тебе удастся выразить зависимый тип на шаблонах для какого то простого случая (а может и для непростого ,при должных затратах труда), сделать ты всё равно с этим ничего не сможешь. Так что смысла в этом нет.
Исправление AndreyKl, :
Матан не в типах, а в доказательстве.
Ты понимаешь, тут штука сложнее. Это две стороны одной медали.
Т.е. когда ты пишешь с зависимыми типами, ты либо ими пользуешься, но тогда ты _обязан_ работать с доказательствами (либо в стиле идриса, либо в стиле кока). Либо ты пытаешься обходится без доказательств (ну, по недостатку умения например), но тогда всё сползает к более обычным типам.
Т.е. как пример
after : (xs ys : list a) -> (length xs < length ys) -> list a
after (x::xs) (y::ys) prf = after xs ys (congr S prf)
after [] ys _ = ys
Конкретно
prf имеет тип lenght(x::xs) < length(y::ys), а (congr S prf) - это доказательство того, что если lenght(x::xs) < length(y::ys), то и length(xs) < length(ys)Соответсвенно, на следующий уровень рекурсии уже передаётся доказательство того что
length(xs) < length(ys).А в конце мы имеем «бесплатно» доказательство того что список не пуст
0 < length(ys).Но тип нашей функции не возвращает эту информацию. Хотя при вызове (другой) функции от данного списка это освободило бы нас от проверки на пустоту.
Лучше было бы как то так:
after : (xs ys : list a) -> (length xs < length ys) -> (zs : list a * 0 < length zs)
after (x::xs) (y::ys) prf = after xs ys (congr S prf)
after [] ys prf = (ys, prf)
Но чтобы это понимать (т.е. написать тип), надо понимать как доказывать, иначе не получится ни передать во внутрь, ни вернуть.
Кстати, насчёт с++, я не зря в начале нашего с тобой разговора упомянул что в курсе что можно изобразить, но на брэйнфаке тоже можно писать программы. Так это я к тому что как ты будешь на с++ со всей этой машинерией работать? Кок показывает все типы и цели и их изменения (от применения тактик), идрис тоже самое.
А что с++? Как работать там со всем этим? Я честно говоря думаю что это будет не просто боль, а адская боль. По русски говоря, не смотря на то что тебе удастся выразить зависимый тип на шаблонах для какого то простого случая (а может и для непростого ,при должных затратах труда), сделать ты всё равно с этим ничего не сможешь. Так что смысла в этом нет.
Исходная версия AndreyKl, :
Матан не в типах, а в доказательстве. В типах слегка напрягает излишний boilerplate, если сравнивать с refined типами, как в LH или Racket, но это реально вопрос привычки.
Ты понимаешь, тут штука сложнее. Это две стороны одной медали.
Т.е. когда ты пишешь с зависимыми типами, ты либо ими пользуешься, но тогда ты _обязан_ работать с доказательствами (либо в стиле идриса, либо в стиле кока). Либо ты пытаешься обходится без доказательств (ну, по недостатку умения например), но тогда всё сползает к более обычным типам.
Т.е. как пример
after : (xs ys : list a) -> (length xs < length ys) -> list a
after (x::xs) (y::ys) prf = after xs ys (congr S prf)
after [] ys _ = ys
Конкретно
prf имеет тип lenght(x::xs) < length(y::ys), а (congr S prf) - это доказательство того, что если lenght(x::xs) < length(y::ys), то и length(xs) < length(ys)Соответсвенно, на следующий уровень рекурсии уже передаётся доказательство того что
length(xs) < length(ys).А в конце мы имеем «бесплатно» доказательство того что список не пуст
0 < length(ys).Но тип нашей функции не возвращает эту информацию. Хотя при вызове (другой) функции от данного списка это освободило бы нас от проверки на пустоту.
Лучше было бы как то так:
after : (xs ys : list a) -> (length xs < length ys) -> (zs : list a * 0 < length zs)
after (x::xs) (y::ys) prf = after xs ys (congr S prf)
after [] ys prf = (ys, prf)
Но чтобы это понимать (т.е. написать тип), надо понимать как доказывать, иначе не получится ни передать во внутрь, ни вернуть.
Кстати, насчёт с++, я не зря в начале нашего с тобой разговора упомянул что в курсе что можно изобразить, но на брэйнфаке тоже можно писать программы. Так это я к тому что как ты будешь на с++ со всей этой машинерией работать? Кок показывает все типы и цели и их изменения (от применения тактик), идрис тоже самое.
А что с++? Как работать там со всем этим? Я честно говоря думаю что это будет не просто боль, а адская боль. По русски говоря, не смотря на то что тебе удастся выразить зависимый тип на шаблонах для какого то простого случая (а может и для непростого ,при должных затратах труда), сделать ты всё равно с этим ничего не сможешь. Так что смысла в этом нет.