Narrowing variable type at run time

Learning
1

is there a way to narrow a variable type at runtime
similar to using type predicates in typescript?

for example, logically I would like to do something like this:

match var with
| cumbersome expression -> func(var)
| more options…

but in reality I have to write
match var with
| cumbersome expression -> func(cumbersome expression)
| more options…

which is less elegant, because the thing is, func accepts a parameter of type of cumbersome expression which is what var is, the problem is that it is not known at runtime so I get an error.

thanks for the help!

2

Types of all variables are statically known during compilation (and are missing in runtme), so you question is not correctly formulated in the context of OCaml language.

P.S. It could be correct in the context of OCaml’s polymorphic variant types but I’m pretty sure you didn’t have them in mind.

3

I also don’t really understand the text of your question, but if I just look at the code,
it looks like you might be looking for the as keyword ?
As @Kakadu said, it can be useful for open variants, for instance

let only_ab =
  function
  | `A ->
       "a"
  | `B ->
       "b"

let in_fact_only_ab x =
  match x with
  | (`A | `B) ->
      only_ab x
  | `C ->
      "c"

let all_abc =
  function
  | (`A | `B) as ab ->
      only_ab ab
  | `C ->
      "c"

The first function cannot be called on ``C`

utop # in_fact_only_ab `C;;
Line 1, characters 16-18:
Error: This expression has type [> `C ] but an expression was expected of type
         [< `A | `B ]
       The second variant type does not allow tag(s) `C

But it does work with the second function

utop # all_abc `C;;
- : string = "c"

The syntax for patterns is at https://caml.inria.fr/pub/docs/manual-ocaml/patterns.html
Also note that you can typeset your code better by putting it between single backticks (inline),
or three (for a block).

2 Likes
4

In OCaml, there is one way to (that I know of) to narrow the type of a variable at runtime: GADTs. Simple example:

utop # type _ t = A : unit t | B : int t;;
type _ t = A : unit t | B : int t
utop # let handle : type a. a t -> a = function
  | A -> ()
  | B -> 1;;
val handle : 'a t -> 'a = <fun>

So what is happening here is we are defining a GADT, _ t, which can have two variant cases: A or B. A has type unit t and B has type int t.

Then we define a function handle that takes a value of this type and returns some value depending on the exact input type. If you apply the value A then at runtime its type is narrowed from a t (where a is a locally abstract type) to unit t. And if you apply B then its type is narrowed from a t to int t.

GADTs are an advanced topic and probably not the first thing you would reach for in day-to-day situations. See the manual for more details on GADTs.

1 Like