Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

typing of or-pattern could be more general #5515

Closed
vicuna opened this issue Feb 24, 2012 · 7 comments
Closed

typing of or-pattern could be more general #5515

vicuna opened this issue Feb 24, 2012 · 7 comments

Comments

@vicuna
Copy link

vicuna commented Feb 24, 2012

Original bug ID: 5515
Reporter: @lefessan
Assigned to: @garrigue
Status: assigned (set by @garrigue on 2012-02-27T22:21:55Z)
Resolution: open
Priority: normal
Severity: feature
Version: 3.13.0+dev
Category: typing
Monitored by: @hcarty @garrigue

Bug description

Currently, the following pattern does not type-check:

match t with
| IntArray t | FloatArray t -> t.(0)

whereas the equivalent

match t with
| IntArray t -> t.(0)
| FloatArray t -> t.(0)

does type-check. Sometimes, you don't want to duplicate the code nor create a function, but still, you need to.

I would suggest to type-check or-patterns by internally defining a function, putting the expression inside, and duplicating internally the cases:

match ... with A(x1..xn) | B(x1..xn) -> E(x1..xn)

would be type-checked as

let e_E (x1..xn) = E(x1..xn) in
match ... with A(x1..xn) -> e_E (x1..xn) | B(x1..xn) -> e_E (x1..xn)

@vicuna
Copy link
Author

vicuna commented Feb 27, 2012

Comment author: @johnwhitington

Or, to take it to its logical conclusion:

match t with
(IntArray | FloatArray) t -> t.0

@vicuna
Copy link
Author

vicuna commented Feb 27, 2012

Comment author: @garrigue

You didn't include the definition of the type of t.
I am right in assuming this is a GADT?
type _ arr = IntArray : int array -> int arr | FloatArray : float array -> float arr

What you are asking for is removing the restriction on or-patterns for GADT
type variables, and this in a polymorphic way. Phew...
First problem, that's not easy to decide when to do it.
The current approach is just to disable constraint generations in or-patterns.
This means that some GADT patterns are already accepted, as long as there
are no typing conflicts with this weaker approach.
So do you suggest we use typing failure to trigger the duplication?
This would not be very clean.
Moreover, this is a bit uncamlish, as the code generated starts to depend
on the typing...

Honestly, if you want to do that, why not define a local function yourself?
Is this such a frequent programming pattern?

@vicuna
Copy link
Author

vicuna commented Feb 27, 2012

Comment author: @lefessan

@garrigue: No, actually, I was only proposing it for simple variants:

type t = IntArray of int array | FloatArray of float array

@johnwhitington: How would you express something more complex, like

match ... with
| IntArray (len, t) | FloatArray (_, t, len) -> t.(len-1)

@vicuna
Copy link
Author

vicuna commented Feb 28, 2012

Comment author: @garrigue

But with your definition using simple variants, you program is not typable anyway...
I can imagine situations where this would be typable (the code is polymorphic and the value returned does not contain that type), but I see less and less the point.

@vicuna
Copy link
Author

vicuna commented Feb 28, 2012

Comment author: @lefessan

Ok, I simplified it too much. The real one was something like that:

type t1 = int * string
type t2 = int * bool
type t = T1 of t1 | T2 of t2
let pos x = match x with
| T1 pair -> fst pair
| T2 pair -> fst pair

where I would like to put the two patterns in one or-clause.

@vicuna
Copy link
Author

vicuna commented Feb 29, 2012

Comment author: @garrigue

Well, you can already write it

let pos = function T1 (a,) | T2 (a,) -> a

If you really want a problematic case, you can get it with objects

type t1 = <x : int; name : string>
type t2 = <x : int; flag : bool>

However is it really worth introducing a new typing rule.

By the way, the above remark about pattern-matching suggests
that you wouldn't need this feature in presence of active patterns.
That could be another, more exciting, approach.

@github-actions
Copy link

This issue has been open one year with no activity. Consequently, it is being marked with the "stale" label. What this means is that the issue will be automatically closed in 30 days unless more comments are added or the "stale" label is removed. Comments that provide new information on the issue are especially welcome: is it still reproducible? did it appear in other contexts? how critical is it? etc.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Projects
None yet
Development

No branches or pull requests

2 participants