Mantis Bug Tracker

View Issue Details Jump to Notes ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0007877OCamltypingpublic2018-11-26 02:532018-11-26 10:08
Assigned Toyallop 
StatusresolvedResolutionno change required 
PlatformOSOS Version
Product Version4.07.1 
Target VersionFixed in Version 
Summary0007877: Trivial GADT functions are untypable
DescriptionI have attached a file: one where the function "" 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 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. :)
TagsNo tags attached.
Attached Files? file icon [^] (1,259 bytes) 2018-11-26 02:53 [Show Content]
? file icon [^] (580 bytes) 2018-11-26 09:06 [Show Content]
? file icon GADTs.hs [^] (567 bytes) 2018-11-26 09:06

- Relationships

-  Notes
mdl (reporter)
2018-11-26 02:55

I meant "module To_string" rather than "" in the second paragraph--sorry for the extra noise.
yallop (developer)
2018-11-26 07:33

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.
mdl (reporter)
2018-11-26 07:39

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.
mdl (reporter)
2018-11-26 08:47

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.)
lpw25 (developer)
2018-11-26 09:30

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 zero
        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 zero
        type 'a succ = zero

    which would make definitions like your [hd] and [tl] functions unsound.
mdl (reporter)
2018-11-26 10:08

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" [], 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!)


- Issue History
Date Modified Username Field Change
2018-11-26 02:53 mdl New Issue
2018-11-26 02:53 mdl File Added:
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:
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
Powered by Mantis Bugtracker