How much are Peano types used?

[bluddy]

It seems like you use Peano types with gadts for sizes, but it's not clear how much these actually do. Can you point me to an operation in the code that takes advantage of this?

[akabe]

Peano types are implemented as phantom types, not GADTs. I cannot clearly understand what you want to know. Can you explain the details of your question?

[bluddy]

Well the thing is, if you're not using GADTs, there's no reason to have Peano types, right? Each size could just be its own unique type. The point of using Peano types (I think) is to allow some relationship between the type numbers, so that for example if you unsqueeze() a tensor, it'll have one more dimension. This can only be done in OCaml via GADTs or (possibly) functors.

[akabe]

Each size could just be its own unique type.

Yes. The sizes of vectors and matrices can be represented as existential types. However, in OCaml, I think introduction of a new unique type is syntactically heavy (such as functors or first-class modules) and existential types are not useful since they cannot escape their scope as follows:

let f () =
  let module N = Slap.Size.Of_int_dyn(struct let value = 42 end) in
    (* N.value : N.n Slap.Size.t where N.n is an existential type. *)
  N.value (* compile error since N.n escapes its scope *)

Slap provides Peano types as easy-to-use size types without above problems. As you said, programmers can use some relationship between the type numbers, but it's not the reason Peano types are supplied.

If existential type had simpler syntax and were able to escape its scope in OCaml, Slap would not need Peano types.

[akabe]

This issue seems to have been solved due to no reply. Please re-open the issue if it isn't solved.