|Anonymous | Login | Signup for a new account||2018-12-15 09:55 CET|
|Main | My View | View Issues | Change Log | Roadmap|
|View Issue Details|
|ID||Project||Category||View Status||Date Submitted||Last Update|
|0007877||OCaml||typing||public||2018-11-26 02:53||2018-11-26 10:08|
|Status||resolved||Resolution||no change required|
|Target Version||Fixed in Version|
|Summary||0007877: Trivial GADT functions are untypable|
|Description||I have attached a file: one where the function "Tl.tl" types, and one where the function "To_string.to_string" types; each file needs a slightly different definition of "t" in order for the corresponding function to typecheck. But no amount of annotation seems to allow for a "t" that can type both some version of "tl" and "to_string".|
Just as a sanity check, I tried writing an equivalent of to_string.ml in GHC Haskell using its GADTs extension, and I can get "tl" to type there, so I don't *think* I'm doing something wrong, but if I am, then sorry for the support ticket masquerading as a bug. :)
|Tags||No tags attached.|
|Attached Files|| bug.ml [^] (1,259 bytes) 2018-11-26 02:53 [Show Content]
fix.ml [^] (580 bytes) 2018-11-26 09:06 [Show Content]
GADTs.hs [^] (567 bytes) 2018-11-26 09:06
|I meant "module To_string" rather than "to_string.ml" in the second paragraph--sorry for the extra noise.|
I don't see anything that suggests a compiler bug here, but there are a few problems in your code, so your question belongs elsewhere (e.g. the mailing list or the online forum).
Here's some advice before you do ask elsewhere: (1) think carefully about what your type definitions actually mean. Once you have the types right, everything else willbecome easier. (2) for the moment, stop using '_' in type definitions, and use named type variables instead.
I would appreciate a little civility; I already said that if I'm making a mistake, then I'm sorry. Would you like to tell me what it is, or is it more entertaining for you to simply lord it over me? Is this how you normally treat people who submit bugs in good faith?
I did in fact try using named type variables. I also tried multiple OCaml versions to see if this was a regression, as I saw similar code online that suggested what I was doing did work at some point.
The "problem" (?) turned out to be that not defining constructors on "zero" and "succ" made the otherwise correct definition for "t" (in "module To_string") fail with the following error:
In this definition, a type variable cannot be deduced
from the type parameters.
So the problem partly involved needing named type variables, but I don't see why "zero" or "succ" require the addition of constructors that are not even being used anywhere in the code. I'll attach the working OCaml version as well as the Haskell code, which may help others who come across this issue, or you, if you decide there's actually an issue here (feel free to consider it a documentation bug, if you prefer.)
I don't think @yallop was being uncivil or lording it over to you. His answer reads like what a teacher would say when trying to lead a student towards an answer rather without giving it outright, presumably because they think that the student will learn more that way. I can see why you might just want a more direct answer, but that doesn't mean that @yallop was being rude by taking a more pedagogical approach.
I'm happy to give a more direct answer, but I'm not entirely sure what you are trying to do with the `Tl.t` type so you'd need to give some explanation of what you are trying to do there. Your `To_string.t` type is clearer, and for that you seem to have a couple of issues:
1. The definition of Cons needs to use a type variable where you have two `_`s. Otherwise there is nothing connecting the length of the list with the length of its tail.
2. You need to give some constructors to the [zero] and [succ] types. Currently they are abstract and could stand for any type definition. By adding constructors you rule out definitions like:
type 'a succ = int
which would make the [_] in your definition of [Cons] unconnected to the parameters of [t] -- this is what the error message you got is saying.
It also rules out definitions like:
type 'a succ = zero
which would make definitions like your [hd] and [tl] functions unsound.
Thank you. This is much more helpful, and again, my intent was not to place this in the wrong venue. I should have explained myself better regarding [Tl.t]: obviously it was incorrect, but I supplied it for sake of showing that it gave a "working" [Tl.tl], albeit with a suspicious signature.
I was further confused by the behavior of the types I'd written for [zero] and [succ]--it didn't occur to me that they weren't behaving as I had intended; I was not considering the module system, and that even without a sharing constraint, "empty" type declarations are in fact *abstract* in a structure--this makes sense now.
I apologize for the earlier frustrated reply, but this interaction here is admittedly subtle, between the cryptic error message and the subtle interaction with module system concerns. (I have respected both your work from a distance, so I was a little taken aback--I'm aware of the restrictions that various module system constructs impose, e.g. why higher-kinded types require the indirections outlined in the paper you authored with @yallop a few years ago, the things your work on modular implicits are intended to solve, related work in 1ML, etc.--but I'm willing to admit this was a brain-fart on my part!)
|2018-11-26 02:53||mdl||New Issue|
|2018-11-26 02:53||mdl||File Added: bug.ml|
|2018-11-26 02:55||mdl||Note Added: 0019484|
|2018-11-26 07:33||yallop||Note Added: 0019485|
|2018-11-26 07:33||yallop||Status||new => resolved|
|2018-11-26 07:33||yallop||Resolution||open => no change required|
|2018-11-26 07:33||yallop||Assigned To||=> yallop|
|2018-11-26 07:39||mdl||Note Added: 0019486|
|2018-11-26 08:47||mdl||Note Added: 0019487|
|2018-11-26 09:06||mdl||File Added: fix.ml|
|2018-11-26 09:06||mdl||File Added: GADTs.hs|
|2018-11-26 09:30||lpw25||Note Added: 0019488|
|2018-11-26 10:08||mdl||Note Added: 0019489|
|Copyright © 2000 - 2011 MantisBT Group|