How to declare a function signature as a datatype?

Learning
1

Hi there,
I am studying Modern Compiler Implementation in ML. I noticed ML supports type declaration like below.

datatype exp = 
  | Ex of Tree.exp
  | Nx of Tree.stm
  | Cx of Temp.label * Temp.label -> Tree.stm

I am trying to declare it in OCaml. However the type Cx is quite interesting because it is actually a function signature. OCaml will pop an error

The type constructor Tree.stm expects 0 argument(s), but is here applied to 1 argument(s)

It seems that Tree.stm is treated as a function instead of a type.

My question is: Is there any way to declare a function signature as a datatype in OCaml?

Also, I tried to modify it to

type exp = 
  | Ex of Tree.exp
  | Nx of Tree.stm
  | Cx of Temp.label -> Temp.label -> Tree.stm
;;

where OCaml function signature obeys. It does not work either. And the error is the same.

2

I’m no expert in GADTs, but I suspect you’ve tripped over them. If I modify your type thus:

type exp = 
  | Ex of exp
  | Nx of stm
  | Cx of (label * label -> stm)

and stm = STM and label = LABEL
;;

it compiles fine with OCaml 4.14.0. Note the parens in the Cx branch.

2 Likes
3

Wow awesome! It does work! Many thanks to you :slight_smile: !

4

The error message is not because @Tom_H accidentally used GADT syntax, as far as I know you need : to tell the language “this is a gadt” and they still used of. Curiously enough, the error message reported here and the error message thrown by my version of the compiler are different. Mine just highlights the arrow and says “syntax error”. I find it treating Tree.stm as a type constructor assuming its input is the code present here surprising.

BTW, @Tom_H, both a * b -> c and a -> b -> c are valid (and theoretically equivalent) SML and OCaml function types. The use of either is simply by convention in the respective languages. In many SML implementations it happens that a * b -> c is slightly more efficient than a -> b -> c because the language has a (strictly specified) left-to-right argument evaluation order.

1 Like
5

Thank you for your reply! Actually I didn’t know much about GADT and just tried to write the type as a function signature.

You are right, both a * b -> c and a -> b -> c works. I was wondering the difference between them and your explanation is just in time! Thank you again for your thoughtful explanation :slight_smile: