* When is a function polymorphic? @ 2005-03-30 22:31 Yaron Minsky 2005-03-31 0:37 ` [Caml-list] " Jacques Garrigue 0 siblings, 1 reply; 12+ messages in thread From: Yaron Minsky @ 2005-03-30 22:31 UTC (permalink / raw) To: Caml Mailing List I don't understand the following results. It seems like these two examples should have the same type. In this example, there isn't much of a difference between the two cases, but there are cases where this idiom is quite convenient. Any idea how to salvage it? # function Some x -> Some () | None as x -> x;; - : 'a option -> unit option = <fun> # function Some x -> Some () | x -> x;; - : unit option -> unit option = <fun> Yaron ^ permalink raw reply [flat|nested] 12+ messages in thread
* Re: [Caml-list] When is a function polymorphic? 2005-03-30 22:31 When is a function polymorphic? Yaron Minsky @ 2005-03-31 0:37 ` Jacques Garrigue 2005-03-31 0:51 ` Yaron Minsky 0 siblings, 1 reply; 12+ messages in thread From: Jacques Garrigue @ 2005-03-31 0:37 UTC (permalink / raw) To: yminsky, yminsky; +Cc: caml-list From: Yaron Minsky <yminsky@gmail.com> > I don't understand the following results. It seems like these two > examples should have the same type. In this example, there isn't much > of a difference between the two cases, but there are cases where this > idiom is quite convenient. Any idea how to salvage it? > > # function Some x -> Some () | None as x -> x;; > - : 'a option -> unit option = <fun> > # function Some x -> Some () | x -> x;; > - : unit option -> unit option = <fun> The typechecker does something special about "as x" patterns. Namely, rather than unifying the type of x with the type of the whole input, it types the aliased pattern twice, and only unifies type parameters which appear in the pattern. So this means that # function Some _ as x -> x | None -> Some () ;; - : unit option -> unit option = <fun> since the type parameter appears in the argument to Some, while # function Some x -> Some () | None as x -> x;; - : 'a option -> unit option = <fun> since it doesn't appear in None. This clever typing only happens with "<pat> as <var>" patterns, so your second example gets the standard result (it is assumed that x could be anything, including Some, as the typing does not use the result of the exhaustiveness analysis.) Jacques Garrigue ^ permalink raw reply [flat|nested] 12+ messages in thread
* Re: [Caml-list] When is a function polymorphic? 2005-03-31 0:37 ` [Caml-list] " Jacques Garrigue @ 2005-03-31 0:51 ` Yaron Minsky 2005-03-31 1:15 ` Eric Cooper ` (2 more replies) 0 siblings, 3 replies; 12+ messages in thread From: Yaron Minsky @ 2005-03-31 0:51 UTC (permalink / raw) To: Jacques Garrigue; +Cc: caml-list On Thu, 31 Mar 2005 09:37:24 +0900 (JST), Jacques Garrigue <garrigue@math.nagoya-u.ac.jp> wrote: > > The typechecker does something special about "as x" patterns. > Namely, rather than unifying the type of x with the type of the whole > input, it types the aliased pattern twice, and only unifies type > parameters which appear in the pattern. So this means that > # function Some _ as x -> x | None -> Some () ;; > - : unit option -> unit option = <fun> > since the type parameter appears in the argument to Some, while > # function Some x -> Some () | None as x -> x;; > - : 'a option -> unit option = <fun> > since it doesn't appear in None. > This clever typing only happens with "<pat> as <var>" patterns, so > your second example gets the standard result (it is assumed that x > could be anything, including Some, as the typing does not use the > result of the exhaustiveness analysis.) > I think I screwed up the original examples a bit. I think the effect I'm looking at doesn't depend on the "as" notation in particular. Here's another example that doesn't use "as": # function Some x -> Some () | None -> None;; - : 'a option -> unit option = <fun> # function Some x -> Some () | x -> x;; - : unit option -> unit option = <fun> The reason I want this is for the following example. Consider some complicated union type with a single parameter: type 'a foo = A of 'a | B of int | C of string * string | ... | ZZ of float I want a function that converts an 'a foo to a unit foo. I tried to write it this way: function A _ -> A () | x -> x But this ends up having type: unit foo -> unit foo, which isn't what I want at all. Any idea of how to achieve this cleanly? Yaron ^ permalink raw reply [flat|nested] 12+ messages in thread
* Re: [Caml-list] When is a function polymorphic? 2005-03-31 0:51 ` Yaron Minsky @ 2005-03-31 1:15 ` Eric Cooper 2005-03-31 1:26 ` Martin Jambon 2005-03-31 2:42 ` Jacques Garrigue 2 siblings, 0 replies; 12+ messages in thread From: Eric Cooper @ 2005-03-31 1:15 UTC (permalink / raw) To: caml-list, caml-list On Wed, Mar 30, 2005 at 07:51:04PM -0500, Yaron Minsky wrote: > Consider some complicated union type with a single parameter: > > type 'a foo = A of 'a | B of int | C of string * string | ... | ZZ of float > > I want a function that converts an 'a foo to a unit foo. I tried to > write it this way: > > function A _ -> A () | x -> x > > But this ends up having type: unit foo -> unit foo, which isn't what I > want at all. Any idea of how to achieve this cleanly? If you can accept another level of constructors, this will work: type 'a foo = A of 'a | NotA of bar and bar = B of int | C of string | D of bool | ... function A _ -> A () | NotA x -> NotA x -- Eric Cooper e c c @ c m u . e d u ^ permalink raw reply [flat|nested] 12+ messages in thread
* Re: [Caml-list] When is a function polymorphic? 2005-03-31 0:51 ` Yaron Minsky 2005-03-31 1:15 ` Eric Cooper @ 2005-03-31 1:26 ` Martin Jambon 2005-03-31 2:42 ` Jacques Garrigue 2 siblings, 0 replies; 12+ messages in thread From: Martin Jambon @ 2005-03-31 1:26 UTC (permalink / raw) To: yminsky; +Cc: Jacques Garrigue, caml-list On Wed, 30 Mar 2005, Yaron Minsky wrote: > I think I screwed up the original examples a bit. I think the effect > I'm looking at doesn't depend on the "as" notation in particular. > Here's another example that doesn't use "as": > > # function Some x -> Some () | None -> None;; > - : 'a option -> unit option = <fun> > # function Some x -> Some () | x -> x;; > - : unit option -> unit option = <fun> > > The reason I want this is for the following example. Consider some > complicated union type with a single parameter: > > type 'a foo = A of 'a | B of int | C of string * string | ... | ZZ of float > > I want a function that converts an 'a foo to a unit foo. I tried to > write it this way: > > function A _ -> A () | x -> x > > But this ends up having type: unit foo -> unit foo, which isn't what I > want at all. Any idea of how to achieve this cleanly? With polymorphic variants, you can do something like this: # type const = [ `B of int | `C ];; type const = [ `B of int | `C ] # type 'a poly = [ `A of 'a | const ];; type 'a poly = [ `A of 'a | `B of int | `C ] # let f : 'a poly -> unit poly= function `A _ -> `A () | #const as x -> x;; val f : 'a poly -> unit poly = <fun> Martin -- Martin Jambon, PhD http://martin.jambon.free.fr ^ permalink raw reply [flat|nested] 12+ messages in thread
* Re: [Caml-list] When is a function polymorphic? 2005-03-31 0:51 ` Yaron Minsky 2005-03-31 1:15 ` Eric Cooper 2005-03-31 1:26 ` Martin Jambon @ 2005-03-31 2:42 ` Jacques Garrigue 2005-03-31 4:04 ` Yaron Minsky 2 siblings, 1 reply; 12+ messages in thread From: Jacques Garrigue @ 2005-03-31 2:42 UTC (permalink / raw) To: yminsky, yminsky; +Cc: caml-list From: Yaron Minsky <yminsky@gmail.com> > I think I screwed up the original examples a bit. I think the effect > I'm looking at doesn't depend on the "as" notation in particular. > Here's another example that doesn't use "as": > > # function Some x -> Some () | None -> None;; > - : 'a option -> unit option = <fun> > # function Some x -> Some () | x -> x;; > - : unit option -> unit option = <fun> > > The reason I want this is for the following example. Consider some > complicated union type with a single parameter: > > type 'a foo = A of 'a | B of int | C of string * string | ... | ZZ of float > > I want a function that converts an 'a foo to a unit foo. I tried to > write it this way: > > function A _ -> A () | x -> x > > But this ends up having type: unit foo -> unit foo, which isn't what I > want at all. Any idea of how to achieve this cleanly? The effect you are looking for does depend on the "as" notation. Here is how to write it: function A _ -> A () | (B _ | C _ | ... | ZZ _) as x -> x Note that the exhaustivity checker will correctly detect that you second case is complete, and the pattern-matching compiler will just branch on wheter the tag is A or not. I.e. no code will be produced to check the second pattern. As others pointed, polymorphic variants allow you to write it in a shorter way, because you can define a type abbreviation for the remaining cases, but in the end it uses the same "as" mechanism. Jacques Garrigue ^ permalink raw reply [flat|nested] 12+ messages in thread
* Re: [Caml-list] When is a function polymorphic? 2005-03-31 2:42 ` Jacques Garrigue @ 2005-03-31 4:04 ` Yaron Minsky 2005-03-31 8:32 ` Jacques Garrigue 0 siblings, 1 reply; 12+ messages in thread From: Yaron Minsky @ 2005-03-31 4:04 UTC (permalink / raw) To: Jacques Garrigue; +Cc: caml-list Interesting. I guess this is best understood as a limitation of the type-checking algorithm. Does anyone know if there are any plans to remove this limitation? Are there fundamental reasons why it would be difficult to do so? Yaron On Thu, 31 Mar 2005 11:42:53 +0900 (JST), Jacques Garrigue <garrigue@math.nagoya-u.ac.jp> wrote: > From: Yaron Minsky <yminsky@gmail.com> > > > I think I screwed up the original examples a bit. I think the effect > > I'm looking at doesn't depend on the "as" notation in particular. > > Here's another example that doesn't use "as": > > > > # function Some x -> Some () | None -> None;; > > - : 'a option -> unit option = <fun> > > # function Some x -> Some () | x -> x;; > > - : unit option -> unit option = <fun> > > > > The reason I want this is for the following example. Consider some > > complicated union type with a single parameter: > > > > type 'a foo = A of 'a | B of int | C of string * string | ... | ZZ of float > > > > I want a function that converts an 'a foo to a unit foo. I tried to > > write it this way: > > > > function A _ -> A () | x -> x > > > > But this ends up having type: unit foo -> unit foo, which isn't what I > > want at all. Any idea of how to achieve this cleanly? > > The effect you are looking for does depend on the "as" notation. > Here is how to write it: > > function A _ -> A () | (B _ | C _ | ... | ZZ _) as x -> x > > Note that the exhaustivity checker will correctly detect that you > second case is complete, and the pattern-matching compiler will just > branch on wheter the tag is A or not. I.e. no code will be produced to > check the second pattern. > > As others pointed, polymorphic variants allow you to write it in a > shorter way, because you can define a type abbreviation for the > remaining cases, but in the end it uses the same "as" mechanism. > > Jacques Garrigue > ^ permalink raw reply [flat|nested] 12+ messages in thread
* Re: [Caml-list] When is a function polymorphic? 2005-03-31 4:04 ` Yaron Minsky @ 2005-03-31 8:32 ` Jacques Garrigue 2005-03-31 12:04 ` Yaron Minsky ` (2 more replies) 0 siblings, 3 replies; 12+ messages in thread From: Jacques Garrigue @ 2005-03-31 8:32 UTC (permalink / raw) To: yminsky, yminsky; +Cc: caml-list From: Yaron Minsky <yminsky@gmail.com> > Interesting. I guess this is best understood as a limitation of the > type-checking algorithm. Does anyone know if there are any plans to > remove this limitation? Are there fundamental reasons why it would be > difficult to do so? This is not a limitation of the type checking algorithm per se. Rather, the type checking algorithm prefers not to use exhaustiveness information when this can be avoided, to keep it predictable. (Exhaustiveness is only used for polymorphic variants, but for a deeper reason.) Is it so difficult to make the extra constructors explicit? Jacques Garrigue ^ permalink raw reply [flat|nested] 12+ messages in thread
* Re: [Caml-list] When is a function polymorphic? 2005-03-31 8:32 ` Jacques Garrigue @ 2005-03-31 12:04 ` Yaron Minsky 2005-03-31 12:48 ` Fermin Reig 2005-03-31 12:16 ` Jon Harrop 2005-04-01 16:26 ` Luc Maranget 2 siblings, 1 reply; 12+ messages in thread From: Yaron Minsky @ 2005-03-31 12:04 UTC (permalink / raw) To: Jacques Garrigue; +Cc: caml-list On Thu, 31 Mar 2005 17:32:23 +0900 (JST), Jacques Garrigue <garrigue@math.nagoya-u.ac.jp> wrote: > From: Yaron Minsky <yminsky@gmail.com> > > > Interesting. I guess this is best understood as a limitation of the > > type-checking algorithm. Does anyone know if there are any plans to > > remove this limitation? Are there fundamental reasons why it would be > > difficult to do so? > > This is not a limitation of the type checking algorithm per se. > Rather, the type checking algorithm prefers not to use > exhaustiveness information when this can be avoided, to keep it > predictable. > (Exhaustiveness is only used for polymorphic variants, but for > a deeper reason.) I guess I'm somewhat out of my depth. I don't quite understand what you mean by exhaustiveness information, and I don't see why avoiding it improves predictability. Do you have an example in mind? > Is it so difficult to make the extra constructors explicit? I'd say there are two issues. The first is that it really can be a pain for large variant types, particularly when the contents of those types are changing during development, and you don't want the function in question to depend on anything other than the particular variants being modified. The second issue is that it just seems like a violation of the principle of least surprise. The fact that this fails to compile: # function Some x -> Some (float x) | x -> x;; This expression has type int option but is here used with type float option but that this does compile: # function Some x -> Some (float x) | None as x -> x;; was quite unexpected, at least by me. That said, it's not all that bad. It just seems confusing, and since I don't see the downside of accepting both functions as type-safe, I don't understand why it's not done. y ^ permalink raw reply [flat|nested] 12+ messages in thread
* Re: [Caml-list] When is a function polymorphic? 2005-03-31 12:04 ` Yaron Minsky @ 2005-03-31 12:48 ` Fermin Reig 0 siblings, 0 replies; 12+ messages in thread From: Fermin Reig @ 2005-03-31 12:48 UTC (permalink / raw) To: yminsky; +Cc: caml-list On Thu, 2005-03-31 at 13:04, Yaron Minsky wrote: > On Thu, 31 Mar 2005 17:32:23 +0900 (JST), Jacques Garrigue > > Is it so difficult to make the extra constructors explicit? > > I'd say there are two issues. The first is that it really can be a > pain for large variant types, particularly when the contents of those > types are changing during development, and you don't want the function > in question to depend on anything other than the particular variants > being modified. > [...] In my code, I try to avoid catchall '_' and 'x' patterns when possible. I end up with long 'or' patterns, such as | (A _ | B _ | C _ | ...) -> ... This style, while more verbose, has one advantage: if I later add a new constructor to my type, the exhaustiveness analysis warns me of all places where I should check. (In fact, this is most useful during development, since that's when type definitions change.) Regarding the typing of # function Some x -> Some () | None -> None;; # function Some x -> Some () | x -> x;; both Haskell and SML do the same as Ocaml, but, unlike Ocaml, neither gives a polymorphic type when using an 'as x' pattern. Fermin This message has been checked for viruses but the contents of an attachment may still contain software viruses, which could damage your computer system: you are advised to perform your own checks. Email communications with the University of Nottingham may be monitored as permitted by UK legislation. ^ permalink raw reply [flat|nested] 12+ messages in thread
* Re: [Caml-list] When is a function polymorphic? 2005-03-31 8:32 ` Jacques Garrigue 2005-03-31 12:04 ` Yaron Minsky @ 2005-03-31 12:16 ` Jon Harrop 2005-04-01 16:26 ` Luc Maranget 2 siblings, 0 replies; 12+ messages in thread From: Jon Harrop @ 2005-03-31 12:16 UTC (permalink / raw) To: caml-list On Thursday 31 March 2005 09:32, Jacques Garrigue wrote: > Is it so difficult to make the extra constructors explicit? But there are _n_ of them! ;-) Cheers, Jon. ^ permalink raw reply [flat|nested] 12+ messages in thread
* Re: [Caml-list] When is a function polymorphic? 2005-03-31 8:32 ` Jacques Garrigue 2005-03-31 12:04 ` Yaron Minsky 2005-03-31 12:16 ` Jon Harrop @ 2005-04-01 16:26 ` Luc Maranget 2 siblings, 0 replies; 12+ messages in thread From: Luc Maranget @ 2005-04-01 16:26 UTC (permalink / raw) To: Jacques Garrigue; +Cc: yminsky, yminsky, caml-list > From: Yaron Minsky <yminsky@gmail.com> > > > Interesting. I guess this is best understood as a limitation of the > > type-checking algorithm. Does anyone know if there are any plans to > > remove this limitation? Are there fundamental reasons why it would be > > difficult to do so? > > This is not a limitation of the type checking algorithm per se. > Rather, the type checking algorithm prefers not to use > exhaustiveness information when this can be avoided, to keep it > predictable. > (Exhaustiveness is only used for polymorphic variants, but for > a deeper reason.) Besides, the test for exhautiveness much relies on typing having been performed. (Except for variants, which undergo a preliminary, specific kind of exhautiveness checking before typing). -- Luc Maranget ^ permalink raw reply [flat|nested] 12+ messages in thread
end of thread, other threads:[~2005-04-01 16:26 UTC | newest] Thread overview: 12+ messages (download: mbox.gz / follow: Atom feed) -- links below jump to the message on this page -- 2005-03-30 22:31 When is a function polymorphic? Yaron Minsky 2005-03-31 0:37 ` [Caml-list] " Jacques Garrigue 2005-03-31 0:51 ` Yaron Minsky 2005-03-31 1:15 ` Eric Cooper 2005-03-31 1:26 ` Martin Jambon 2005-03-31 2:42 ` Jacques Garrigue 2005-03-31 4:04 ` Yaron Minsky 2005-03-31 8:32 ` Jacques Garrigue 2005-03-31 12:04 ` Yaron Minsky 2005-03-31 12:48 ` Fermin Reig 2005-03-31 12:16 ` Jon Harrop 2005-04-01 16:26 ` Luc Maranget
This is a public inbox, see mirroring instructions for how to clone and mirror all data and code used for this inbox; as well as URLs for NNTP newsgroup(s).