Я не верю, что это можно сделать в целом, потому что вы не можете найти подходящее соответствие для функций.Вы также не можете проверить тип функции.Это не то, что зависимые типы.Как и в Haskell или OCaml, единственное, что вы можете сделать с функцией, это применить ее к какому-либо аргументу.Тем не менее, я разработал некоторый трюк, который мог бы сделать:
myFun : {a, b : Type} -> (a -> b) -> List Type
myFun {a} {b} _ = [a, b]
Теперь проблема в том, что a -> b - единственная подпись, которая будет соответствовать любой произвольной функции.Но, конечно, он не ведет себя так, как вы хотели бы для функций с арностью выше единицы:
> myFun (+)
[Integer, Integer -> Integer] : List Type
Так что для извлечения большего количества типов аргументов потребуется какой-то рекурсивный вызов самого себя:
myFun : {a, b : Type} -> (a -> b) -> List Type
myFun {a} {b} _ = a :: myFun b
Проблема здесь в том, что b - это произвольный тип, не обязательно тип функции, и я никак не могу понять, чтобы динамически проверить, является ли это функцией или нет, так что я полагаю, что этостолько, сколько вы можете сделать с Idris.
Однако динамическая проверка типов (по крайней мере, на мой взгляд) не является желательной функцией в статически типизированном языке.В конце концов, весь смысл статической типизации состоит в том, чтобы заранее указать , какие аргументы может обрабатывать функция, и предотвратить вызов функций с недопустимыми аргументами во время компиляции.Так что, в принципе, вам это вообще не нужно.Если бы вы указали, в чем заключалась ваша грандиозная цель, кто-то, вероятно, показал бы вам правильный способ сделать это.