Skip to content

Instantly share code, notes, and snippets.

@vrotaru
Last active Aug 29, 2015
Embed
What would you like to do?
type _ ty =
| TBool : bool ty
| TInt : int ty
type _ value =
| Bool : bool -> bool value
| Int : int -> int value
type _ expr =
| Value : 'a value -> 'a expr
| If : bool expr * 'a expr * 'a expr -> 'a expr
| Eq : 'a expr * 'a expr -> bool expr
| Lt : int expr * int expr -> bool expr
type any =
| Any : _ expr -> any
let rec type_from_expr: type a. a expr -> a ty = function
| Value(Bool _) -> TBool
| Value(Int _) -> TInt
| Eq(l, r) -> TBool
| Lt(l, r) -> TBool
| If(c, tb, _) -> type_from_expr tb
let rec expr_from_any: type a. a ty -> any -> a expr = fun t a ->
match t, a with
| TBool, Any(Value(Bool b)) -> Value (Bool b)
| TInt, Any(Value(Int n)) -> Value (Int n)
| TBool, Any(Eq(l, r)) -> Eq(l, r)
| TBool, Any(Lt(l, r)) -> Lt(l, r)
| t, Any(If(c,l, r)) ->
let l' = expr_from_any t (Any l) in
let r' = expr_from_any t (Any r) in
If (c, l', r')
| _ -> failwith "Type mismatch"
(* everything above works, but that is not what I wanted to achieve *)
(* the function below, does not typecheck *)
let unany: type a. any -> a expr = fun x ->
try
expr_from_any TBool x (* this expression has type 'a expr, but an expression was expected of type a expr *)
with Failure s
-> expr_from_any TInt x (* same as above *)
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment