| Anonymous | Login | Signup for a new account | 2013-05-26 03:45 CEST | ![]() |
| Main | My View | View Issues | Change Log | Roadmap |
| View Issue Details [ Jump to Notes ] | [ Issue History ] [ Print ] | ||||||||||
| ID | Project | Category | View Status | Date Submitted | Last Update | ||||||
| 0005515 | OCaml | OCaml typing | public | 2012-02-24 10:50 | 2012-02-29 09:39 | ||||||
| Reporter | lefessan | ||||||||||
| Assigned To | garrigue | ||||||||||
| Priority | normal | Severity | feature | Reproducibility | have not tried | ||||||
| Status | assigned | Resolution | open | ||||||||
| Platform | OS | OS Version | |||||||||
| Product Version | 3.13.0+dev | ||||||||||
| Target Version | Fixed in Version | ||||||||||
| Summary | 0005515: typing of or-pattern could be more general | ||||||||||
| 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) | ||||||||||
| Tags | No tags attached. | ||||||||||
| Attached Files | |||||||||||
Notes |
|
|
(0006975) johnwhitington (reporter) 2012-02-27 18:49 |
Or, to take it to its logical conclusion: match t with (IntArray | FloatArray) t -> t.0 |
|
(0006986) garrigue (manager) 2012-02-27 23:44 |
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? |
|
(0006987) lefessan (developer) 2012-02-27 23:49 |
@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) |
|
(0006990) garrigue (manager) 2012-02-28 09:49 |
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. |
|
(0006992) lefessan (developer) 2012-02-28 14:22 |
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. |
|
(0006997) garrigue (manager) 2012-02-29 09:39 |
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. |
Issue History |
|||
| Date Modified | Username | Field | Change |
| 2012-02-24 10:50 | lefessan | New Issue | |
| 2012-02-27 18:49 | johnwhitington | Note Added: 0006975 | |
| 2012-02-27 23:21 | garrigue | Assigned To | => garrigue |
| 2012-02-27 23:21 | garrigue | Status | new => assigned |
| 2012-02-27 23:44 | garrigue | Note Added: 0006986 | |
| 2012-02-27 23:49 | lefessan | Note Added: 0006987 | |
| 2012-02-28 09:49 | garrigue | Note Added: 0006990 | |
| 2012-02-28 14:22 | lefessan | Note Added: 0006992 | |
| 2012-02-29 09:39 | garrigue | Note Added: 0006997 | |
| Copyright © 2000 - 2011 MantisBT Group |