Simplest way to recognize a primitive type?

gadt
adt

#1

I was working with GADT (where all is so strongly typed… which is first painful then gives satisfaction).
Going back to a case with ADT type, I felt surprised not to be able to answer to the following question (when pattern matching): how to recognize the primitive type of an OCaml value?

Let’s take a simple (non GADT) example:

type t = A of string * string 
       | B of string * int
val f :  string -> 'a  ->  t

let f (x:string) (y:'a) : t =
   match a with 
     | (* int pattern    *) -> A (x, b)
     | (* string pattern *) -> B (x, b)

How can we recognize the primitive type of the arguments?
Is there a function such as the #show_val directive called in the Toplevel:

let a = "foo";;
#show_val a
(* val a : string *)

As a pattern matching can’t take an int on a branch and a string on another (two different types), my question is weird and reveals that I should obviously be missing something.

let f x = match x with 1 -> true | "a" -> false
                                   ^^^
Error: This pattern matches values of type string
      but a pattern was expected which matches values of type int

A simplified GADT example (with no problem as arguments are easily pattern matched) would be:

type t = A of string * string 
       | B of string * int

type _ expr =
| String : string -> string expr
| Int : int -> int expr
| T : t -> t expr
| Foo : string  * 'a expr -> t expr

let rec eval : type a. a expr -> a = function
| String x -> x
| Int x -> x
| T x -> x
| Foo (x, String y) -> A (x, y)
| Foo (x, Int y) -> B (x, y)
| _ -> failwith "not a valid expression"

I’m surprised to be in trouble with simple ADT case as I begin to be comfortable with GADT!
It looks like I’m trying to use GADT pattern on ADT…

EDIT: the question can also be: “How to do with ADT the above GADT example ?”


#2

I think(bc I’m a Ocaml noob) that pattern matching can only deconstruct types with a constructor or match values of a type.

I say think because I’m not sure that my description of Ocaml’s pattern matching is exhaustive.


#3
type t = A of string * string 
       | B of string * int
val f :  string -> 'a  ->  t

let f (x:string) (y:'a) : t =
   match a with 
     | (* int pattern    *) -> A (x, b)
     | (* string pattern *) -> B (x, b)

It’s possible I misunderstand what you are trying to achieve - maybe you can try to give a bit more context. In any case: the patterns on the left-hand side of a match must have the same type (same as type of a in this case) and hence you can’t match different types. You would need a type that carries the desired values:

type t = A of string * string 
       | B of string * int

type y = Int of int
       | Str of string

let f (x:string) y : t =
   match y with 
     | Int b -> B (x, b)
     | Str b -> A (x, b)

#4

When using type y as you did, the solution is trivial to filter out any input, and the case is closed (it’s the same story, whether it’s ADT or GADT).

Yes, here are more details about the context of my question.
During my exploration, I found interesting (if not useful for real life practice) to get the available type of an OCaml value in the current environment.

I see the following situations:

  1. There is a character flow from a file, a socket or stdin
    -> A lexer+parser can be used to recognize that flow an get an AST that clearly exposes typed values that can then used in many ways (with various pattern matching to do some actions).

  2. The program is defined (types and functions), it compiles and then is used ;
    -> nothing to say, just use the program.

  3. I’m playing with the Toplevel and want to explore all OCaml features (even possibly unsafe ones), visible or more hidden under the hood.

-> My question is in the context of 3.

I asked to my self “BTW, how can I get the type of a value within the current environment?”, but do you know real life situations where getting the type of an object in the environment is of interest?

The following directives available from the Toplevel answer partially my question. They only display the signature of any value or type, but not the value definition

#show_type t (* the same as reading the type *)
#show_val bar (* useless ; shows the value signature, as when typing `bar;;` *)

#show_module_type BIP (* the same as reading the module type ; useful if it's not defined locally *)
#show_module Test (* shows only module signature ; need to go to the module definition to get the stuff packed in the module *)

#show_class_type foo
#show_class bar

#show_exception Not_found;;

Since I created this topic, I’ve been looking around and found the Topdirs and Toploop modules (within Toplevel module).

I think it could be interesting for understanding what’s going on under the hood, and for making some customized Toplevel where can be performed some operations on the types and values defined in the current environment (editing types and values).
Anyway, we can may around because the type checker guarantees the safety of the code (it compiles or not).

Do you know an other or better way to programmatically manipulate types and values of an environment?

This exploration should eventually drive me into studying some parts of the OCaml compiler. However, I find it attractive and also very impressive. Which way would you recommend to have a gentle introduction to the OCaml compiler?


#5

You can take a look at the runtime representation of values using the Obj module. However, it is in general not possible to re-create the exact type declaration from the runtime presentation alone. In particular, you can’t recreate the names of type constructors. Chapter Memory Representation of Values in Real World OCaml provides some background.


#6

I noticed the presence of the famous Obj.magic that seems to be very controversial (in fact, one has to be very aware of this runtime representation of values).
And many discussions in various sites about this undocumented Obj module.

My first goal is to understand what’s going on under the hood when some code is evaluated.
Of course, I could just satisfy myself with just evaluating code as many times as needed, or compiling it.
But, for example, how can I get a list of the values and types in the environment? and the version of the type of a value?
The following happens when one creates an object from a type, changes and evaluates a revised version of that type:

type t = A of int
let t1 = A 1;;
let t2 = A 1;;
t1 = t2;;
(* - : bool = true *)
type t = A of int
let t2 = A 1;;
t1 = t2;;
(*   ^^
     Error: This expression has type t/1689 but an expression was expected of type
     t/1686
*)

#7

The OCaml toplevel and alternatives like utop don’t support introspection like it would be possible in a Smalltalk or Python environment - so I don’t have a good answer here for how to explore the current environment.

As for what you observed: the two types are considered distinct even though they have the same structure. In general, for types to be considered compatible they need to trace back to the same declaration which here isn’t the case but would be the case for a primitive type like string.