Аппликативный функтор в F*: ошибка проверки типа

Question

В качестве эксперимента, пытаясь познакомиться с F*, я попытался реализовать аппликативный функтор. Я застрял в странно выглядящей ошибке проверки типов. Я еще не уверен, связано ли это с какой-то функцией / логикой проверки типов, о которой я не знаю, или это вызвано подлинной ошибкой.

Вот часть кода, которая доставляет мне неприятности:

module Test

noeq type test : Type -> Type =
    | Apply : test ('a -> 'b) -> test 'a -> test 'b

val apply : test ('a -> 'b) -> test 'a -> test 'b
let apply f x = Apply f x

И вот соответствующая ошибка:

Test(7,24-7,25): (Error 54) Test.test 'a is not a subtype of the expected type Test.test 'a (see also Test(7,12-7,13))
1 error was reported (see above)

Может ли кто-нибудь любезно указать мне, что мне не хватает? Повлияет ли подтип на поведение унификации типов? Или это проверка типа и это ошибка компилятора?

Answer 1

Я полагаю, что существует ограничение вселенского неравенства для индуктивов, которое вы не применяете.

Следующий код проверяет тип:

noeq type test : Type0 -> Type =
    | Apply : test ('a -> 'b) -> test 'a -> test 'b

val apply : test ('a -> 'b) -> test 'a -> test 'b
let apply f x = Apply f x

Обратите внимание на 0 Я добавил в первой строке.

Это работает, потому что это говорит о том, что первый Type0 находится в более низкой вселенной, чем Type (что само по себе, я считаю, означает любую вселенную). В вашем случае, F* не знает, как сравнивать юниверсы для этих двух типов, поэтому терпит неудачу.

Если бы вы написали noeq type test : Type -> Type0 вы бы увидели немного лучшее сообщение об ошибке: "Не удалось решить неравенства вселенной для индуктивов". Поэтому я виню здесь сообщение об ошибке.

Я прошу прощения, если объяснение не хватает точности, я не человек PL...:)