Как объявить ограничение hasEq?

Question

Я только начинаю с F*, что означает, что я написал несколько строк вместе с учебником. Пока что это действительно интересно, и я бы хотел продолжить обучение.

Первое, что я попытался сделать самостоятельно, - написать тип, представляющий непустой список. Это была моя попытка:

type nonEmptyList 'a = l : (list 'a) { l <> [] }

Но я получаю ошибку

Не удалось проверить неявный аргумент: проверка подтипа не удалась; ожидаемый тип (a#6468:Type{(hasEq a@0)}); получил тип Тип

Я знаю, что я на правильном пути, потому что, если я ограничу свой тип списка, содержащий строки, это работает:

type nonEmptyList = l : (list string) { l <> [] }

Я предполагаю, что это означает, что l <> [] в исходном примере недействительно, потому что я не указал, что 'a должен поддерживать равенство. Проблема в том, что я не могу понять, как это сделать. Я думаю, это как-то связано с более высоким hasEq, но пытается такие вещи, как:

type nonEmptyList 'a = l : (list 'a) { hasEq 'a /\ l <> [] }

не получил меня никуда. Учебник не распространяется hasEq и я не могу найти ничего полезного в примерах репозитория GitHub, так что теперь я застрял.

Answer 1

Вы правильно определили проблему здесь. Тип 'a что вы использовали в определении nonEmptyList не указано и, следовательно, не может поддерживать равенство. Ваша интуиция верна, вы должны сказать F*, что 'a это тип, который имеет равенство, добавив уточнение к нему:

Для этого вы можете написать следующее:

type nonEmptyList (a:Type{hasEq a}) = l : (list a) { l <> [] }

Обратите внимание, что связующее, которое я использовал для этого типа, a и не 'a, Это может вызвать синтаксическую ошибку, это имеет больше смысла, потому что это больше не "любой" тип. Также обратите внимание, что вы можете быть еще более точным и указать юниверс типа a как Type0 если нужно.

Answer 2

Ваш анализ действительно правильный, и принятый ответ дает правильное решение в целом.

Однако для вашего конкретного примера вам не нужно решаемое равенство в элементах списка: вы можете просто использовать (list 'a){ ~ (List.isEmpty l) },

Для справки вот определение isEmpty:

(** [isEmpty l] returns [true] if and only if [l] is empty  *)
val isEmpty: list 'a -> Tot bool
let isEmpty l = match l with
  | [] -> true
  | _ -> false