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

Теорема о неполноте действительно утверждает что непротиворечивая система неполна. И мы надеемся что зависимые типы - непротиворечивая система. Но штука в том, что в коке можно формулировать утверждения об утверждениях (т.е. переходить на логики более «высоких» уровней). Это, на сколько я понимаю, и в математике происходит. Т.е. можно пытаться рассматривать аксиомы о системе аксиом и об утверждениях в этой (первой) системе аксиом. Ну и пытаться доказать в новой системе требуемое изначально утверждение. Правда в новой системе опять найдётся недоказуемое утверждение. Но можно опять же попробовать создать систему «уровнем выше». И так до бесконечности.

Ладно. Завершимость не так критична. Критично отсутствие необходимости переписывать алгоритм лишь ради удовлетворения типов.

Раз в coq есть гетерогенные списки, можно ли написать тип mapcar, полностью соответствующий его документации (а не обрубать под типизацию)?

То есть, первый аргумент может быть «a designator for a function». То есть это функция или строка, по которой можно найти функцию. Или хотя бы число, по которому можно взять функцию из некоего массива.

Остальные аргументы должны быть гетерогенными списками. Списки могут быть разной длины. Результат будет минимальной длины из аргументов.

То есть удастся ли вообще написать что-то более конкретное, чем (на Haskell)

data Designator a b = S String | F (a -> b)
mapcar :: Designator a b -> [[Dynamic]] -> [Dynamic]

Теорема о неполноте действительно утверждает что непротиворечивая система неполна. И мы надеемся что зависимые типы - непротиворечивая система. Но штука в том, что в коке можно формулировать утверждения об утверждениях (т.е. переходить на логики более «высоких» уровней). Это, на сколько я понимаю, и в математике происходит. Т.е. можно пытаться рассматривать аксиомы о системе аксиом и об утверждениях в этой (первой) системе аксиом. Ну и пытаться доказать в новой системе требуемое изначально утверждение. Правда в новой системе опять найдётся недоказуемое утверждение. Но можно опять же попробовать создать систему «уровнем выше». И так до бесконечности.

Ладно. Завершимость не так критична. Критично отсутствие необходимости переписывать алгоритм лишь ради удовлетворения типов.

Раз в coq есть гетерогенные списки, можно ли написать тип mapcar, полностью соответствующий его документации (а не обрубать под типизацию)?

То есть, первый аргумент может быть «a designator for a function». То есть это функция или строка, по которой можно найти функцию. Или хотя бы число, по которому можно взять функцию из некоего массива.

Остальные аргументы должны быть гетерогенными списками. Списки могут быть разной длины. Результат будет минимальной длины из аргументов.

То есть удастся ли вообще написать что-то более конкретное, чем (на Haskell)

data Designator = S String | F (a -> b)
mapcar :: Designator -> [[Dynamic]] -> [Dynamic]