<div dir="auto"><div>It is Storable that makes Ptr operate as typed pointers. I also think Ptr on its own doesn't have that much about its argument type, so I'm +1 on the proposal.</div><div dir="auto"><br></div><div dir="auto">Btw, shouldn't every type be storable? In current Haskell, Maybes or (->)s aren't Storable, yet in C++, arrays of std::optionals or std::functions are well-defined.</div><div dir="auto"><br></div><div dir="auto">As an exception, for Void, I agree that they must remain not Storable since it has no values.<br><br><div class="gmail_quote" dir="auto"><div dir="ltr">2018년 10월 30일 (화) 08:31, Carter Schonwald <<a href="mailto:carter.schonwald@gmail.com">carter.schonwald@gmail.com</a>>님이 작성:<br></div><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div dir="ltr">the parametricity isn't for when you know things, its for saying "these are possibly different or possibly the same, dont let me mix them up though, cause I dont know yet"<div><br></div></div><br><div class="gmail_quote"><div dir="ltr">On Mon, Oct 29, 2018 at 7:03 PM Daniel Cartwright <<a href="mailto:chessai1996@gmail.com" target="_blank" rel="noreferrer">chessai1996@gmail.com</a>> wrote:<br></div><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div dir="ltr">I'm not sure that argument applies at all, when talking about _incorrect_ usages of Ptr. Sure, Addr probably shouldn't be used when there is meaningful type information/value to recover, but neither should Ptr be used when there is none.<div><br></div><div>The argument being made is not to make 'better', per se, and there definitely won't be a 'mathematical statement' about this, but it certainly may be made clearer - in my opinion, the usages of 'Ptr' that i've already brought up are inherently unclear because of the bogus phantom type associated with 'Ptr'. The illustration of this begs no code that doesn't already exist in corelibs.</div><div><br></div></div><br><div class="gmail_quote"><div dir="ltr">On Mon, Oct 29, 2018 at 6:19 PM Carter Schonwald <<a href="mailto:carter.schonwald@gmail.com" target="_blank" rel="noreferrer">carter.schonwald@gmail.com</a>> wrote:<br></div><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div dir="ltr"><div dir="ltr">to zoom out: what code is improved? what code is made better/clearer? No one has articulated this clearly. <div><br></div><div>The one example of Addr being used in Vector.Storable.Mutable is not an argument in favor of using Addr. Its an argument against it existing.</div><div><br></div><div>i'm looking for evidence, in the form of code i can look at then say "yes, this is better code" when comparing the two. Or a mathematical statement of "what is made better"</div><div><br></div><div><a class="gmail_plusreply" id="m_864893652255671201m_-9079759639542071166m_-8561936842640734714gmail-plusReplyChip-0" href="mailto:david.feuer@gmail.com" target="_blank" rel="noreferrer">@David Feuer</a> , @Daniel , do you have one?<br></div><div><br></div><div>when i'm writing complicated code, MORE polymorphism helps me usually.</div><div><br></div><div>I can write some code like the following and even though I'm using it with Int at argument,</div><div>I *Know* that i'm not mixing up arguments/values that i write as different types. I cannot do this with Address!</div><div>(the type / function below can be found at <a href="https://github.com/wellposed/numerical/blob/3a0bbf50bc6ce0b710aee755f5a4bfce08af4201/src/Numerical/Array/Layout/Builder.hs#L294" target="_blank" rel="noreferrer">https://github.com/wellposed/numerical/blob/3a0bbf50bc6ce0b710aee755f5a4bfce08af4201/src/Numerical/Array/Layout/Builder.hs#L294</a> )</div><div><br>{-# SPECIALIZE INLINE computeStarts :: [(Int,Int)]->Int->Int ->[(Int,Int)] #-}<br>computeStarts:: (Enum a, Ord a, Num b )=>[(a,b)]-> a -> a -> [(a,b)]</div><div><br></div><div>parametricity (even when constrained by type classes) is a powerful and foundational tool for good programming in haskell and similar languages</div><div><br></div><div>there has been nothing stated here that successfully articulates a good reason to forgo/discourage parametricity as an engineering tool. for thats what Addr is. </div><div>A datatype thats never safe in isolation, and discourages using parametricity to write correct software.</div><div><br></div><div>a very strong case is needed to forgo parametricity. </div><div><br></div><div><br></div><div><br><table class="m_864893652255671201m_-9079759639542071166m_-8561936842640734714gmail-highlight m_864893652255671201m_-9079759639542071166m_-8561936842640734714gmail-tab-size m_864893652255671201m_-9079759639542071166m_-8561936842640734714gmail-js-file-line-container" style="box-sizing:border-box;border-spacing:0px;border-collapse:collapse;color:rgb(36,41,46);font-family:-apple-system,system-ui,"Segoe UI",Helvetica,Arial,sans-serif,"Apple Color Emoji","Segoe UI Emoji","Segoe UI Symbol";font-size:14px"><tbody style="box-sizing:border-box"><tr style="box-sizing:border-box"><td id="m_864893652255671201m_-9079759639542071166m_-8561936842640734714gmail-LC292" class="m_864893652255671201m_-9079759639542071166m_-8561936842640734714gmail-blob-code m_864893652255671201m_-9079759639542071166m_-8561936842640734714gmail-blob-code-inner m_864893652255671201m_-9079759639542071166m_-8561936842640734714gmail-js-file-line" style="box-sizing:border-box;padding:0px 10px;line-height:20px;vertical-align:top;overflow:visible"></td></tr></tbody></table></div></div></div><br><div class="gmail_quote"><div dir="ltr">On Mon, Oct 29, 2018 at 5:33 PM David Feuer <<a href="mailto:david.feuer@gmail.com" target="_blank" rel="noreferrer">david.feuer@gmail.com</a>> wrote:<br></div><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div dir="auto">Good point! Call it nominal then.</div><br><div class="gmail_quote"><div dir="ltr">On Mon, Oct 29, 2018, 5:24 PM Carter Schonwald <<a href="mailto:carter.schonwald@gmail.com" target="_blank" rel="noreferrer">carter.schonwald@gmail.com</a>> wrote:<br></div><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div dir="ltr">absolutely false, represeentational equality of the  type a in `Ptr a` does not mean the memory representation at the corresponding address is the same.<div>(it sometimes is true, but memory packing/alignment details in structs in C  for otherwise equivlanet structs should rule this out)</div><div><br></div><div>aka, `a` being representationally equal to `b` via haskell newtypes does not mean the memory representation at `Ptr a`, and `Ptr b` are the same. a trivial example is when</div><div>host and network byte order aren't the same (eg big vs little endian memory encodings)</div></div><br><div class="gmail_quote"><div dir="ltr">On Mon, Oct 29, 2018 at 12:28 PM David Feuer <<a href="mailto:david.feuer@gmail.com" rel="noreferrer noreferrer" target="_blank">david.feuer@gmail.com</a>> wrote:<br></div><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">What? Of course you can dereference it. You dereference it, getting a<br>
value of type `Void`,<br>
and apply absurd to get whatever you want in the world. This, of<br>
course, is utter nonsense,<br>
unless *having* the Ptr Void means that something has already gone<br>
wrong. It's pretty<br>
hard for me to imagine a situation where this is actually what you<br>
want. A Ptr () isn't nonsense.<br>
It is not terrible to use Ptr () to represent an Addr, but I wonder if<br>
it sends the wrong message.<br>
By the way: there's another argument for having Addr in base for now.<br>
We would really<br>
*like* for Ptr's parameter to have a *representational* role, but we<br>
*don't* want to require<br>
unsafeCoerce to cast Ptrs. The solution to that in the current role system:<br>
<br>
    data Addr = Addr Addr#<br>
<br>
    newtype Ptr a = Ptr_ Addr<br>
    type role Ptr representational<br>
<br>
    pattern Ptr :: Addr# -> Ptr a<br>
    pattern Ptr addr# = Ptr_ (Addr addr#)<br>
<br>
    -- Allow users to reveal coercibility of pointer types locally<br>
    ptrCoercion :: Coercion (Ptr a) (Ptr b)<br>
    ptrCoercion = Coercion<br>
<br>
    castPtr :: Ptr a -> Ptr b<br>
    castPtr = coerceWith ptrCoercion -- (or the now-free unwrap-rewrap<br>
definition)<br>
<br>
<br>
So even if we don't *expose* Addr in base, we should almost certainly *define*<br>
it there.<br>
On Mon, Oct 29, 2018 at 12:11 PM Carter Schonwald<br>
<<a href="mailto:carter.schonwald@gmail.com" rel="noreferrer noreferrer" target="_blank">carter.schonwald@gmail.com</a>> wrote:<br>
><br>
> The point , hahah, of a Ptr void is that you can’t dereference it.  But you certainly can cast it and do address arithmetic on it!!<br>
><br>
><br>
><br>
> On Mon, Oct 29, 2018 at 10:10 AM David Feuer <<a href="mailto:david.feuer@gmail.com" rel="noreferrer noreferrer" target="_blank">david.feuer@gmail.com</a>> wrote:<br>
>><br>
>> On Mon, Oct 29, 2018, 10:05 AM Sven Panne <<a href="mailto:svenpanne@gmail.com" rel="noreferrer noreferrer" target="_blank">svenpanne@gmail.com</a>> wrote:<br>
>>><br>
>>> Am Mo., 29. Okt. 2018 um 14:27 Uhr schrieb Daniel Cartwright <<a href="mailto:chessai1996@gmail.com" rel="noreferrer noreferrer" target="_blank">chessai1996@gmail.com</a>>:<br>
>>>><br>
>>>> 'Ptr Void' is not a pointer to a value of type 'Void'; there are no values of type 'Void': this type is nonsensical.<br>
>>><br>
>>><br>
>>> That's the whole point, and it actually makes sense: If you see "Ptr Void", you can't do much with it, apart from passing it around or using castPtr on it. This is exactly what should be achieved by using "Ptr Void" in an API. This is basically the same as "void *" in C/C++.<br>
>><br>
>><br>
>> No, it does not make sense. The approximate equivalent of C's void* is Ptr Any. Ptr Void promises to give you anything you want on dereference, which is nonsense.<br>
>><br>
>>><br>
>>> You can't store or read "()", so the same holds as for Void (which didn't exist when the FFI was created IIRC).<br>
>><br>
>><br>
>> Sure you can. Storing () does nothing and reading it gives (). Our () is somewhat similar to C's void return type.<br>
>> _______________________________________________<br>
>> Libraries mailing list<br>
>> <a href="mailto:Libraries@haskell.org" rel="noreferrer noreferrer" target="_blank">Libraries@haskell.org</a><br>
>> <a href="http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries" rel="noreferrer noreferrer noreferrer" target="_blank">http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries</a><br>
</blockquote></div>
</blockquote></div>
</blockquote></div>
_______________________________________________<br>
Libraries mailing list<br>
<a href="mailto:Libraries@haskell.org" target="_blank" rel="noreferrer">Libraries@haskell.org</a><br>
<a href="http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries" rel="noreferrer noreferrer" target="_blank">http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries</a><br>
</blockquote></div>
</blockquote></div>
_______________________________________________<br>
Libraries mailing list<br>
<a href="mailto:Libraries@haskell.org" target="_blank" rel="noreferrer">Libraries@haskell.org</a><br>
<a href="http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries" rel="noreferrer noreferrer" target="_blank">http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries</a><br>
</blockquote></div></div></div>