4

I'm just starting out with F*, by which I mean I've written a few lines along with the tutorial. So far it's really interesting and I'd like to keep learning.

The first thing I tried to do on my own was to write a type that represents a non-empty list. This was my attempt:

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

But I get the error

Failed to verify implicit argument: Subtyping check failed; expected type (a#6468:Type{(hasEq a@0)}); got type Type

I know I'm on the right track though because, if I constrain my list type to containing strings, this does work:

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

I'm assuming this means that l <> [] in the original example isn't valid because I haven't specified that 'a should support equality. The problem is that I cannot for the life of me figure out how to do that. I guess is has something to do with a higher kind called hasEq, but trying things such as: 

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

hasn't gotten me anywhere. The tutorial doesn't cover hasEq and I can't find anything helpful in the examples in the GitHub repo so now I'm stuck.

Clément
  • 12,299
  • 15
  • 75
  • 115
Richiban
  • 5,569
  • 3
  • 30
  • 42

2 Answers2

4

You correctly identified the problem here. The type 'a that you used in the definition of nonEmptyList is left unspecified and therefore could not support equality. Your intuition is correct, you need to tell F* that 'a is a type that has equality, by adding a refinement on it:

To do that, you can write the following:

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

Note that the binder I used for the type is a and not 'a. It would cause a syntax error, it makes more sense because it isn't "any" type anymore. Also, note that you can be even more precise and specify the universe of the type a as Type0 if needbe.

Benjamin Beurdouche
  • 81
  • 2
  • 1
    Thank you for this! It works, although specifying that `a` supports equality feels like a hack to get what I want. Do you know how I can accomplish this without it? It seems that I can `match` a list value against `[]` without equality, but I can't use the `<>` operator... – Richiban Mar 13 '17 at 10:45
3

Your analysis is indeed correct, and the accepted answer gives the right solution in general.

For your concrete example, though, you don't need decidable equality on list elements: you can just use (list 'a){ ~ (List.isEmpty l) }.

For reference, here's the definition of 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
Clément
  • 12,299
  • 15
  • 75
  • 115
  • Thanks for your answer, Clément. This brings up an interesting question about type systems in general: surely all empty lists are the same? I should be able to compare *any* list to [], even if the contained type of the list does not support equality. – Richiban May 19 '17 at 09:33
  • Right – and that's essentially what isEmpty is doing. – Clément May 19 '17 at 09:44