История изменений
Исправление AndreyKl, (текущая версия) :
И получается, что любая функция с ограничениями должна возвращать пару?
Ну.. как бы, это результат её работы, соответственно - да, выходит что так. Т.е. ликвидхаскель просто выкидывает потом эту инфу, но таки её надо получить чтобы проверить ограничение.
Но если её можно выкинуть на этапе компиляции (т.е. проверка статически можен быть осущетсвлена) , то компилятор выкинет (если дальше не используешь нигде).
А тип пары точно можно описывать через **
Ну в Коке через *, а в идрисе кажется через **.
И как в константу len_x_xs попадает информация про x и r?
len_x_xs (кстати, я не знаю как она в библиотеке называется, чтоб не вводить в заблуждение). Может она и не нужна кстати, но отвечая на вопрос, в общем случае на примере len_x_xs, она описана так:
len_x_xs : {x} -> {xs} -> length xs < length (x::xs)
можно заставить компилятор считать все параметры явными, тогда это будет выглядеть как то так
addElem : a -> (x : List a) -> (r:List a ** length x < length r)
addElem a x = (Cons a x, @len_x_xs a x)
соотвественно, когда параметры неявные, компилятор просто выводит их из типа. Т.е. он видит что тип второго элемента пары (length x < length (a::x)) и понимает что чтобы типы сошлись надо передать len_x_xs a и x. Но не конкретные в рантайме, а просто любые, т.е. любые которые будут переданы функции (т.е. работает примерно как с forall), (я там развернул тип чтобы сошлось).
Исправление AndreyKl, :
И получается, что любая функция с ограничениями должна возвращать пару?
Ну.. как бы, это результат её работы, соответственно - да, выходит что так. Т.е. ликвидхаскель просто выкидывает потом эту инфу, но таки её надо получить чтобы проверить ограничение.
Но если её можно выкинуть на этапе компиляции (т.е. проверка статически можен быть осущетсвлена) , то компилятор выкинет (если дальше не используешь нигде).
А тип пары точно можно описывать через **
Ну в Коке через *, а в идрисе кажется через **.
И как в константу len_x_xs попадает информация про x и r?
len_x_xs (кстати, я не знаю как она в библиотеке называется, чтоб не вводить в заблуждение). Может она и не нужна кстати, но отвечая на вопрос, в общем случае на примере len_x_xs, она описана так:
len_x_xs : {x} -> {xs} -> length xs < length (x::xs)
можно заставить компилятор считать все параметры явными, тогда это будет выглядеть как то так
addElem : a -> (x : List a) -> (r:List a ** length x < length r)
addElem a x = (Cons a x, @len_x_xs a x)
соотвественно, когда параметры неявные, компилятор просто выводит их из типа. Т.е. он видит что тип второго элемента пары (length x < length (a::x)) и понимает что чтобы типы сошлись надо передать len_x_xs a и x. Но не конкретные в рантайме, а просто любые, т.е. любые которые будут переданы функции (вроде как с forall), (я там развернул тип чтобы сошлось).
Исправление AndreyKl, :
И получается, что любая функция с ограничениями должна возвращать пару?
Ну.. как бы, это результат её работы, соответственно - да, выходит что так. Т.е. ликвидхаскель просто выкидывает потом эту инфу, но таки её надо получить чтобы проверить ограничение.
Но если её можно выкинуть на этапе компиляции (т.е. проверка статически можен быть осущетсвлена) , то компилятор выкинет (если дальше не используешь нигде).
А тип пары точно можно описывать через **
Ну в Коке через *, а в идрисе кажется через **.
И как в константу len_x_xs попадает информация про x и r?
len_x_xs (кстати, я не знаю как она в библиотеке называется, чтоб не вводить в заблуждение). Может она и не нужна кстати, но отвечая на вопрос, в общем случае на примере len_x_xs, она описана так:
len_x_xs : {x} -> {xs} -> length xs < length (x::xs)
можно заставить компилятор считать все параметры явными, тогда это будет выглядеть как то так
addElem : a -> (x : List a) -> (r:List a ** length x < length r)
addElem a x = (Cons a x, @len_x_xs a x)
соотвественно, когда параметры неявные, компилятор просто выводит их из типа. Т.е. он видит что тип второго элемента пары (length x < length (a::x)) и понимает что чтобы типы сошлись надо передать len_x_xs a и x. Но не конкретные в рантайме, а просто любые, т.е. любые которые будут переданы функции (вроде как с forall), (я там развернул тип чтобы сошлось).
Исправление AndreyKl, :
И получается, что любая функция с ограничениями должна возвращать пару?
Ну.. как бы, это результат её работы, соответственно - да, выходит что так. Т.е. ликвидхаскель просто выкидывает потом эту инфу, но таки её надо получить чтобы проверить ограничение.
Но если её можно выкинуть на этапе компиляции (т.е. проверка статически можен быть осущетсвлена) , то компилятор выкинет (если дальше не используешь нигде).
А тип пары точно можно описывать через **
Ну в Коке через *, а в идрисе кажется через **.
И как в константу len_x_xs попадает информация про x и r?
len_x_xs (кстати, я не знаю как она в библиотеке называется, чтоб не вводить в заблуждение). Может она и не нужна кстати, но отвечая на вопрос, в общем случае на примере len_x_xs, она описана так:
len_x_xs : {x} -> {xs} -> length xs < length (x::xs)
можно заставить компилятор считать все параметры явными, тогда это будет выглядеть так
addElem : a -> (x : List a) -> (r:List a ** length x < length r)
addElem a x = (Cons a x, len_x_xs a x)
соотвественно, когда параметры неявные, компилятор просто выводит их из типа. Т.е. он видит что тип второго элемента пары (length x < length (a::x)) и понимает что чтобы типы сошлись надо передать len_x_xs a и x. Но не конкретные в рантайме, а просто любые, т.е. любые которые будут переданы функции (вроде как с forall), (я там развернул тип чтобы сошлось).
Исходная версия AndreyKl, :
И получается, что любая функция с ограничениями должна возвращать пару?
Ну.. как бы, это результат её работы, соответственно - да, выходит что так. Т.е. ликвидхаскель просто выкидывает потом эту инфу, но таки её надо получить чтобы проверить ограничение.
Но если её можно выкинуть на этапе компиляции (т.е. проверка статически можен быть осущетсвлена) , то компилятор выкинет (если дальше не используешь нигде).
А тип пары точно можно описывать через **
Ну в Коке через *, а в идрисе кажется через **.
И как в константу len_x_xs попадает информация про x и r?
len_x_xs (кстати, я не знаю как она в библиотеке называется, чтоб не вводить в заблуждение). Может она и не нужна кстати, но отвечая на вопрос, в общем случае на примере len_x_xs, она описана так:
len_x_xs : {x} -> {xs} -> length xs < length (x::xs)
можно заставить компилятор считать все параметры явными, тогда это будет выглядеть так
addElem : a -> (x : List a) -> (r:List a ** length r > length x)
addElem a x = (Cons a x, len_x_xs a x)
соотвественно, когда параметры неявные, компилятор просто выводит их из типа. Т.е. он видит что тип второго элемента пары (length r > length x) и понимает что чтобы типы сошлись надо передать len_x_xs a и x. Но не конкретные в рантайме, а просто любые, т.е. любые которые будут переданы функции (вроде как с forall).