When is a function polymorphic?

When is a function polymorphic?

[Yaron Minsky]

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

Re: [Caml-list] When is a function polymorphic?

[Jacques Garrigue]

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

Re: [Caml-list] When is a function polymorphic?

[Yaron Minsky]

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

Re: [Caml-list] When is a function polymorphic?

[Eric Cooper]

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

Re: [Caml-list] When is a function polymorphic?

[Martin Jambon]

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

Re: [Caml-list] When is a function polymorphic?

[Jacques Garrigue]

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

Re: [Caml-list] When is a function polymorphic?

[Yaron Minsky]

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
>

Re: [Caml-list] When is a function polymorphic?

[Jacques Garrigue]

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

Re: [Caml-list] When is a function polymorphic?

[Yaron Minsky]

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

Re: [Caml-list] When is a function polymorphic?

[Fermin Reig]

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.

Re: [Caml-list] When is a function polymorphic?

[Jon Harrop]

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.

Re: [Caml-list] When is a function polymorphic?

[Luc Maranget]

> 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