Polymorphic variant restriction in the variant definition
Suppose that I want to model a simple expression type in OCaml:
type expr =
| `Int of int
| `Str of string
| `IntAdd of expr * expr
| `StrAdd of expr * expr
Is it possible to restrict expr in expr * expr to specific constructors of expr itself (i.e. I'd like IntExpr to only allow 'Int's)? I can mimic this with pattern
matching but it gets cumbersome after expr expands. Can I somehow
use OCaml's type system to achieve this?
I tried using polymorphic type upper bounds as follows:
type expr =
| `Int of int
| `Str of string
| `IntAdd of [< `Int] * [< `Int]
| `StrAdd of [< `Str] * [< `Str]
but compiler does not accept this (with message In case IntAdd of [< Int ] * ([< Int ] as 'a) the variable 'a is unbound). Is there any trick to make this work?
types ocaml polymorphic-variants
asked Nov 10 at 2:56
Ibrahim
132
add a comment |
Suppose that I want to model a simple expression type in OCaml:
type expr =
| `Int of int
| `Str of string
| `IntAdd of expr * expr
| `StrAdd of expr * expr
Is it possible to restrict expr in expr * expr to specific constructors of expr itself (i.e. I'd like IntExpr to only allow 'Int's)? I can mimic this with pattern
matching but it gets cumbersome after expr expands. Can I somehow
use OCaml's type system to achieve this?
I tried using polymorphic type upper bounds as follows:
type expr =
| `Int of int
| `Str of string
| `IntAdd of [< `Int] * [< `Int]
| `StrAdd of [< `Str] * [< `Str]
but compiler does not accept this (with message In case IntAdd of [< Int ] * ([< Int ] as 'a) the variable 'a is unbound). Is there any trick to make this work?
types ocaml polymorphic-variants
asked Nov 10 at 2:56
Ibrahim
132
This seems like the kind of thing you'd use GADTs for in Haskell:data Expr a where Int :: Int -> Expr Int; Str :: String -> Expr String; IntAdd :: Expr Int -> Expr Int -> Expr Int; StrAdd :: Expr String -> Expr String -> Expr String
– melpomene
Nov 10 at 3:23
1
mads-hartmann.com/ocaml/2015/01/05/…
– melpomene
Nov 10 at 3:57
Last link really helped a lot---thanks!
– Ibrahim
Nov 14 at 16:07
add a comment |
Suppose that I want to model a simple expression type in OCaml:
type expr =
| `Int of int
| `Str of string
| `IntAdd of expr * expr
| `StrAdd of expr * expr
Is it possible to restrict expr in expr * expr to specific constructors of expr itself (i.e. I'd like IntExpr to only allow 'Int's)? I can mimic this with pattern
matching but it gets cumbersome after expr expands. Can I somehow
use OCaml's type system to achieve this?
I tried using polymorphic type upper bounds as follows:
type expr =
| `Int of int
| `Str of string
| `IntAdd of [< `Int] * [< `Int]
| `StrAdd of [< `Str] * [< `Str]
but compiler does not accept this (with message In case IntAdd of [< Int ] * ([< Int ] as 'a) the variable 'a is unbound). Is there any trick to make this work?
types ocaml polymorphic-variants
asked Nov 10 at 2:56
Ibrahim
132
Suppose that I want to model a simple expression type in OCaml:
type expr =
| `Int of int
| `Str of string
| `IntAdd of expr * expr
| `StrAdd of expr * expr
Is it possible to restrict expr in expr * expr to specific constructors of expr itself (i.e. I'd like IntExpr to only allow 'Int's)? I can mimic this with pattern
matching but it gets cumbersome after expr expands. Can I somehow
use OCaml's type system to achieve this?
I tried using polymorphic type upper bounds as follows:
type expr =
| `Int of int
| `Str of string
| `IntAdd of [< `Int] * [< `Int]
| `StrAdd of [< `Str] * [< `Str]
but compiler does not accept this (with message In case IntAdd of [< Int ] * ([< Int ] as 'a) the variable 'a is unbound). Is there any trick to make this work?
types ocaml polymorphic-variants
types ocaml polymorphic-variants
asked Nov 10 at 2:56
Ibrahim
132
asked Nov 10 at 2:56
Ibrahim
132
asked Nov 10 at 2:56
Ibrahim
132
asked Nov 10 at 2:56
Ibrahim
132
asked Nov 10 at 2:56
Ibrahim
132
132
This seems like the kind of thing you'd use GADTs for in Haskell:data Expr a where Int :: Int -> Expr Int; Str :: String -> Expr String; IntAdd :: Expr Int -> Expr Int -> Expr Int; StrAdd :: Expr String -> Expr String -> Expr String
– melpomene
Nov 10 at 3:23
1
mads-hartmann.com/ocaml/2015/01/05/…
– melpomene
Nov 10 at 3:57
Last link really helped a lot---thanks!
– Ibrahim
Nov 14 at 16:07
add a comment |
This seems like the kind of thing you'd use GADTs for in Haskell:data Expr a where Int :: Int -> Expr Int; Str :: String -> Expr String; IntAdd :: Expr Int -> Expr Int -> Expr Int; StrAdd :: Expr String -> Expr String -> Expr String
– melpomene
Nov 10 at 3:23
1
mads-hartmann.com/ocaml/2015/01/05/…
– melpomene
Nov 10 at 3:57
Last link really helped a lot---thanks!
– Ibrahim
Nov 14 at 16:07
This seems like the kind of thing you'd use GADTs for in Haskell:
data Expr a where Int :: Int -> Expr Int; Str :: String -> Expr String; IntAdd :: Expr Int -> Expr Int -> Expr Int; StrAdd :: Expr String -> Expr String -> Expr String – melpomene
Nov 10 at 3:23
This seems like the kind of thing you'd use GADTs for in Haskell:
data Expr a where Int :: Int -> Expr Int; Str :: String -> Expr String; IntAdd :: Expr Int -> Expr Int -> Expr Int; StrAdd :: Expr String -> Expr String -> Expr String – melpomene
Nov 10 at 3:23
1
1
mads-hartmann.com/ocaml/2015/01/05/…
– melpomene
Nov 10 at 3:57
mads-hartmann.com/ocaml/2015/01/05/…
– melpomene
Nov 10 at 3:57
Last link really helped a lot---thanks!
– Ibrahim
Nov 14 at 16:07
Last link really helped a lot---thanks!
– Ibrahim
Nov 14 at 16:07
add a comment |
1 Answer
1
active
oldest
votes
The given example is simple enough for polymorphic variants to suffice:
type int_expr = [`Int of int | `Add of int_expr * int_expr]
type string_expr = [`String of string | `Concat of string_expr * string_expr]
type expr = [int_expr | string_expr]
If you want more interesting features like polymorphic data structures, GADTs are necessary:
type _ expr =
| Int : int -> int expr
| Add : int expr * int expr -> int expr
| String : string -> string expr
| Concat : string expr * string expr -> string expr
| Pair : 'a expr * 'b expr -> ('a * 'b) expr
| Fst : ('a * 'b) expr -> 'a expr
| Snd : ('a * 'b) expr -> 'b expr
Inference and comprehensibility of error messages suffers with GADTs, so be prepared to work to overcome those difficulties if you decide to use them.
answered Nov 10 at 6:57
gsg
7,81911118
Thanks--- GADTs seem like a proper way to do this.
– Ibrahim
Nov 14 at 16:01
Side note: first example with polymorphic variants does not work as I'd prefer it, as`Add(`String("a"), `String("b"))compiles w/o any issues.
– Ibrahim
Nov 14 at 16:03
@Ibrahim, of course, polymorphic variants allow unconstrained construction by design. Note that the value you describe will not have typeexpr, and you will get a type error at the point you try to use it as anexpr, rather than at the point of construction. You can use annotations if you want earlier type checks.
– gsg
Nov 16 at 5:01
add a comment |
Your Answer
StackExchange.ifUsing("editor", function ()
StackExchange.using("externalEditor", function ()
StackExchange.using("snippets", function ()
StackExchange.snippets.init();
);
);
, "code-snippets");
StackExchange.ready(function()
var channelOptions =
tags: "".split(" "),
id: "1"
;
initTagRenderer("".split(" "), "".split(" "), channelOptions);
StackExchange.using("externalEditor", function()
// Have to fire editor after snippets, if snippets enabled
if (StackExchange.settings.snippets.snippetsEnabled)
StackExchange.using("snippets", function()
createEditor();
);
else
createEditor();
);
function createEditor()
StackExchange.prepareEditor(
heartbeatType: 'answer',
autoActivateHeartbeat: false,
convertImagesToLinks: true,
noModals: true,
showLowRepImageUploadWarning: true,
reputationToPostImages: 10,
bindNavPrevention: true,
postfix: "",
imageUploader:
brandingHtml: "Powered by u003ca class="icon-imgur-white" href="https://imgur.com/"u003eu003c/au003e",
contentPolicyHtml: "User contributions licensed under u003ca href="https://creativecommons.org/licenses/by-sa/3.0/"u003ecc by-sa 3.0 with attribution requiredu003c/au003e u003ca href="https://stackoverflow.com/legal/content-policy"u003e(content policy)u003c/au003e",
allowUrls: true
,
onDemand: true,
discardSelector: ".discard-answer"
,immediatelyShowMarkdownHelp:true
);
);
Sign up or log in
StackExchange.ready(function ()
StackExchange.helpers.onClickDraftSave('#login-link');
);
Sign up using Google
Sign up using Facebook
Sign up using Email and Password
Post as a guest
Required, but never shown
StackExchange.ready(
function ()
StackExchange.openid.initPostLogin('.new-post-login', 'https%3a%2f%2fstackoverflow.com%2fquestions%2f53235639%2fpolymorphic-variant-restriction-in-the-variant-definition%23new-answer', 'question_page');
);
Post as a guest
Required, but never shown
1 Answer
1
active
oldest
votes
1 Answer
1
active
oldest
votes
active
oldest
votes
active
oldest
votes
The given example is simple enough for polymorphic variants to suffice:
type int_expr = [`Int of int | `Add of int_expr * int_expr]
type string_expr = [`String of string | `Concat of string_expr * string_expr]
type expr = [int_expr | string_expr]
If you want more interesting features like polymorphic data structures, GADTs are necessary:
type _ expr =
| Int : int -> int expr
| Add : int expr * int expr -> int expr
| String : string -> string expr
| Concat : string expr * string expr -> string expr
| Pair : 'a expr * 'b expr -> ('a * 'b) expr
| Fst : ('a * 'b) expr -> 'a expr
| Snd : ('a * 'b) expr -> 'b expr
Inference and comprehensibility of error messages suffers with GADTs, so be prepared to work to overcome those difficulties if you decide to use them.
answered Nov 10 at 6:57
gsg
7,81911118
Thanks--- GADTs seem like a proper way to do this.
– Ibrahim
Nov 14 at 16:01
Side note: first example with polymorphic variants does not work as I'd prefer it, as`Add(`String("a"), `String("b"))compiles w/o any issues.
– Ibrahim
Nov 14 at 16:03
@Ibrahim, of course, polymorphic variants allow unconstrained construction by design. Note that the value you describe will not have typeexpr, and you will get a type error at the point you try to use it as anexpr, rather than at the point of construction. You can use annotations if you want earlier type checks.
– gsg
Nov 16 at 5:01
add a comment |
The given example is simple enough for polymorphic variants to suffice:
type int_expr = [`Int of int | `Add of int_expr * int_expr]
type string_expr = [`String of string | `Concat of string_expr * string_expr]
type expr = [int_expr | string_expr]
If you want more interesting features like polymorphic data structures, GADTs are necessary:
type _ expr =
| Int : int -> int expr
| Add : int expr * int expr -> int expr
| String : string -> string expr
| Concat : string expr * string expr -> string expr
| Pair : 'a expr * 'b expr -> ('a * 'b) expr
| Fst : ('a * 'b) expr -> 'a expr
| Snd : ('a * 'b) expr -> 'b expr
Inference and comprehensibility of error messages suffers with GADTs, so be prepared to work to overcome those difficulties if you decide to use them.
answered Nov 10 at 6:57
gsg
7,81911118
Thanks--- GADTs seem like a proper way to do this.
– Ibrahim
Nov 14 at 16:01
Side note: first example with polymorphic variants does not work as I'd prefer it, as`Add(`String("a"), `String("b"))compiles w/o any issues.
– Ibrahim
Nov 14 at 16:03
@Ibrahim, of course, polymorphic variants allow unconstrained construction by design. Note that the value you describe will not have typeexpr, and you will get a type error at the point you try to use it as anexpr, rather than at the point of construction. You can use annotations if you want earlier type checks.
– gsg
Nov 16 at 5:01
add a comment |
The given example is simple enough for polymorphic variants to suffice:
type int_expr = [`Int of int | `Add of int_expr * int_expr]
type string_expr = [`String of string | `Concat of string_expr * string_expr]
type expr = [int_expr | string_expr]
If you want more interesting features like polymorphic data structures, GADTs are necessary:
type _ expr =
| Int : int -> int expr
| Add : int expr * int expr -> int expr
| String : string -> string expr
| Concat : string expr * string expr -> string expr
| Pair : 'a expr * 'b expr -> ('a * 'b) expr
| Fst : ('a * 'b) expr -> 'a expr
| Snd : ('a * 'b) expr -> 'b expr
Inference and comprehensibility of error messages suffers with GADTs, so be prepared to work to overcome those difficulties if you decide to use them.
answered Nov 10 at 6:57
gsg
7,81911118
The given example is simple enough for polymorphic variants to suffice:
type int_expr = [`Int of int | `Add of int_expr * int_expr]
type string_expr = [`String of string | `Concat of string_expr * string_expr]
type expr = [int_expr | string_expr]
If you want more interesting features like polymorphic data structures, GADTs are necessary:
type _ expr =
| Int : int -> int expr
| Add : int expr * int expr -> int expr
| String : string -> string expr
| Concat : string expr * string expr -> string expr
| Pair : 'a expr * 'b expr -> ('a * 'b) expr
| Fst : ('a * 'b) expr -> 'a expr
| Snd : ('a * 'b) expr -> 'b expr
Inference and comprehensibility of error messages suffers with GADTs, so be prepared to work to overcome those difficulties if you decide to use them.
answered Nov 10 at 6:57
gsg
7,81911118
answered Nov 10 at 6:57
gsg
7,81911118
answered Nov 10 at 6:57
gsg
7,81911118
answered Nov 10 at 6:57
gsg
7,81911118
7,81911118
Thanks--- GADTs seem like a proper way to do this.
– Ibrahim
Nov 14 at 16:01
Side note: first example with polymorphic variants does not work as I'd prefer it, as`Add(`String("a"), `String("b"))compiles w/o any issues.
– Ibrahim
Nov 14 at 16:03
@Ibrahim, of course, polymorphic variants allow unconstrained construction by design. Note that the value you describe will not have typeexpr, and you will get a type error at the point you try to use it as anexpr, rather than at the point of construction. You can use annotations if you want earlier type checks.
– gsg
Nov 16 at 5:01
add a comment |
Thanks--- GADTs seem like a proper way to do this.
– Ibrahim
Nov 14 at 16:01
Side note: first example with polymorphic variants does not work as I'd prefer it, as`Add(`String("a"), `String("b"))compiles w/o any issues.
– Ibrahim
Nov 14 at 16:03
@Ibrahim, of course, polymorphic variants allow unconstrained construction by design. Note that the value you describe will not have typeexpr, and you will get a type error at the point you try to use it as anexpr, rather than at the point of construction. You can use annotations if you want earlier type checks.
– gsg
Nov 16 at 5:01
Thanks--- GADTs seem like a proper way to do this.
– Ibrahim
Nov 14 at 16:01
Thanks--- GADTs seem like a proper way to do this.
– Ibrahim
Nov 14 at 16:01
Side note: first example with polymorphic variants does not work as I'd prefer it, as
`Add(`String("a"), `String("b")) compiles w/o any issues.– Ibrahim
Nov 14 at 16:03
Side note: first example with polymorphic variants does not work as I'd prefer it, as
`Add(`String("a"), `String("b")) compiles w/o any issues.– Ibrahim
Nov 14 at 16:03
@Ibrahim, of course, polymorphic variants allow unconstrained construction by design. Note that the value you describe will not have type
expr, and you will get a type error at the point you try to use it as an expr, rather than at the point of construction. You can use annotations if you want earlier type checks.– gsg
Nov 16 at 5:01
@Ibrahim, of course, polymorphic variants allow unconstrained construction by design. Note that the value you describe will not have type
expr, and you will get a type error at the point you try to use it as an expr, rather than at the point of construction. You can use annotations if you want earlier type checks.– gsg
Nov 16 at 5:01
add a comment |
Thanks for contributing an answer to Stack Overflow!
- Please be sure to answer the question. Provide details and share your research!
But avoid …
- Asking for help, clarification, or responding to other answers.
- Making statements based on opinion; back them up with references or personal experience.
To learn more, see our tips on writing great answers.
Some of your past answers have not been well-received, and you're in danger of being blocked from answering.
Please pay close attention to the following guidance:
- Please be sure to answer the question. Provide details and share your research!
But avoid …
- Asking for help, clarification, or responding to other answers.
- Making statements based on opinion; back them up with references or personal experience.
To learn more, see our tips on writing great answers.
Sign up or log in
StackExchange.ready(function ()
StackExchange.helpers.onClickDraftSave('#login-link');
);
Sign up using Google
Sign up using Facebook
Sign up using Email and Password
Post as a guest
Required, but never shown
StackExchange.ready(
function ()
StackExchange.openid.initPostLogin('.new-post-login', 'https%3a%2f%2fstackoverflow.com%2fquestions%2f53235639%2fpolymorphic-variant-restriction-in-the-variant-definition%23new-answer', 'question_page');
);
Post as a guest
Required, but never shown
Sign up or log in
StackExchange.ready(function ()
StackExchange.helpers.onClickDraftSave('#login-link');
);
Sign up using Google
Sign up using Facebook
Sign up using Email and Password
Post as a guest
Required, but never shown
Sign up or log in
StackExchange.ready(function ()
StackExchange.helpers.onClickDraftSave('#login-link');
);
Sign up using Google
Sign up using Facebook
Sign up using Email and Password
Post as a guest
Required, but never shown
Sign up or log in
StackExchange.ready(function ()
StackExchange.helpers.onClickDraftSave('#login-link');
);
Sign up using Google
Sign up using Facebook
Sign up using Email and Password
Sign up using Google
Sign up using Facebook
Sign up using Email and Password
Post as a guest
Required, but never shown
Required, but never shown
Required, but never shown
Required, but never shown
Required, but never shown
Required, but never shown
Required, but never shown
Required, but never shown
Required, but never shown
This seems like the kind of thing you'd use GADTs for in Haskell:
data Expr a where Int :: Int -> Expr Int; Str :: String -> Expr String; IntAdd :: Expr Int -> Expr Int -> Expr Int; StrAdd :: Expr String -> Expr String -> Expr String– melpomene
Nov 10 at 3:23
1
mads-hartmann.com/ocaml/2015/01/05/…
– melpomene
Nov 10 at 3:57
Last link really helped a lot---thanks!
– Ibrahim
Nov 14 at 16:07