Как я могу реализовать функцию typeOf?

Question

Как я могу реализовать функцию typeOf?

Поскольку в Idris типы являются первоклассными, кажется, что я должен написать typeOf функция, которая возвращает тип своего аргумента:

typeOf : a => a -> Type
typeOf x = a

Однако, когда я пытаюсь вызвать эту функцию, я получаю то, что выглядит как ошибка:

*example> typeOf 42
Can't find implementation for Integer

Как я могу правильно реализовать это typeOf функционировать? Или есть что-то более тонкое в идее "получения типа значения", которое я упускаю, что предотвратило бы существование такой функции?

3

function types idris first-class

Источник

user5044950 23 июл '17 в 00:43

1 ответ

Решение

Другие вопросы по тегам function types idris first-class

user1068232 23 июл '17 в 09:17 2017-07-23 09:17 · Accepted Answer · 2017-07-23 09:17

Запишите это так:

typeOf : {a : Type} -> a -> Type
typeOf {a} _ = a

a => b является функцией, которая имеет неявный аргумент, заполненный разрешением интерфейса. {a : b} -> c является функцией с неявным аргументом, заполненным объединением.

Здесь нет необходимости ссылаться на интерфейсы. Каждый термин имеет один тип. Если ты пишешь typeOf 42неявное a подразумевается Integer путем объединения.