au-ts / cogent

Cogent Project
https://trustworthy.systems/projects/TS/cogent.pml
Other
158 stars 26 forks source link

Documentation says record types are sensitive to field order. #313

Closed gteege closed 4 years ago

gteege commented 4 years ago

But they are not. The default layout orders fields alphabetically, so the order of specifying fields is irrelevant. The implementation accepts record types with the same fields specified in different order as equivalent.

You should change the documentation (5.3 Composite types -> Record types, 2nd and 3rd sentence). I will change the manual accordingly.

wom-bat commented 4 years ago

I personally think this is a bug. It makes it really hard to debug a cogent program by comparing code with a core dump, it makes it harder (without dargent) to share variables between C and cogent.

zilinc commented 4 years ago

In principle, users should never know (or have to care about) the layout that the Cogent compiler picks (the default layout, so to speak). If a specific layout is needed, use Dargent. This design principle makes sense to me, because Cogent itself doesn't specify data layout and the default layout can be changed as the compiler evolves without breaking any user code.

In practice, to improve usability, a c-compat layout keyword can be added to Dargent, so that it just picks what the users "think" it should be, laying out datatypes in a natural way (e.g. inserts paddings, preserves filed order, etc.). But following this line of arguments, why don't we just make the default layout to be identical to c-compat? I can't think of any good reasons.

So I reached this self-contradicting reasoning...

zilinc commented 4 years ago

Relevant: #291