<div dir="ltr"><div class="gmail_extra"><div class="gmail_quote">On Wed, Oct 28, 2015 at 9:19 AM, Richard Eisenberg <span dir="ltr"><<a href="mailto:eir@cis.upenn.edu" target="_blank">eir@cis.upenn.edu</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left-width:1px;border-left-color:rgb(204,204,204);border-left-style:solid;padding-left:1ex">I don't have terribly much to add, but I do want to counter one point:<br>
<span class=""><br>
On Oct 28, 2015, at 5:48 AM, Edward Kmett <<a href="mailto:ekmett@gmail.com">ekmett@gmail.com</a>> wrote:<br>
> There are situations where we are truly polymorphic in lifting, e.g. (==) from Eq and compare from Ord don't care if the arguments of type 'a' are lifted or not.<br>
<br>
</span>But these do, I think. In running code, if (==) is operating over a lazy type, it has to check if the pointer points to a thunk. If (==) is operating over a strict one, it can skip the check. This is not a big difference, but it *is* a difference.<br></blockquote><div><br></div><div>Yes, but this is the job of the particular instance. Remember the instance gets to know the type it is working at, and its corresponding levity.</div><div><br></div><div>class Eq (l :: Levity) (t :: Type l) where</div><div> (==) :: a -> a -> Bool</div><div><br></div><div>instance Eq @Unlifted (SmallMutableArray s a) where</div><div> (==) = sameSmallMutableArray</div><div><br></div><div>instance Eq @Lifted [] where</div><div> (==) = ...</div><div><br></div><div>Your objection arises for things like</div><div><br></div><div>instance Eq @l (Foo @l)</div><div><br></div><div>Where the same code has to execute with different levities, but if I can't even case or seq on a value with polymorphic levity, and can't construct such a value but merely pass it around then such code is still sound. It isn't safe to write functions that return values of polymorphic levity. I can however hand them back as (# a #). This is how we handle indexing into a array today.</div><div><br></div><div>If we had a Maybe that was levity polymorphic in its argument </div><div><br></div><div>Maybe :: forall (l :: Levity). Type l -> Lifted<br></div><div><br></div><div>instance Eq @l a => Eq @Lifted (Maybe @l a) where</div><div> Just a == Just b = a == b</div><div> _ == _ = False</div><div><br></div><div>is still okay under these rules, it never case analyzes a value of polymorphic levity, never seq's it. Neither of those things is legal because you can't 'enter' the closure.</div><div><br></div><div>If it was levity polymorphic in the result type</div><div><br></div><div>Maybe :: forall (i :: Levity) (j :: Levity). Type i -> Type j</div><div><br></div><div>then your objection comes true.</div><div><br></div><div>I can't naively write:</div><div><br></div><div><font color="#ff0000">instance Eq @i a => Eq j (Maybe @i @j a) where</font></div><div><font color="#ff0000"> Just a == Just b = a == b</font></div><div><font color="#ff0000"> _ == _ = False</font></div><div><br></div><div>without compiling the same code twice, because of the act of case analysis.</div><div><br></div><div>If we don't have real 'strict data types' in Lifted this situation never arises though.</div><div><br></div><div>Even if we do I can write separate:</div><div><br></div><div><div>instance Eq @i a => Eq Lifted (Maybe @i Lifted a) </div></div><div><div>instance Eq @i a => Eq Unlifted (Maybe @i Unlifted a) </div></div><div><br></div><div>instances, unless we can do better by writing a class constraint on the levity that we can use in a clever way here.</div><div><br></div><div>I'm mostly concerned with the middle case where we don't overload data types on their levity, and try to recover the ability to talk about strict data types by other more explicit means, but rather permit them to accept arguments of different levities. There none of the code I care about actually needs to act differently based on levity. <br></div><div><br></div><div>Anything that results in a function space there has to care about levity, but until a type occurs on the right hand side of an (->) or I go to seq a value of that type or case analyze it, I don't need to care about if its lifted or unlifted.</div><div><br></div><div>With Dan's (!S) then things get more complicated in ways I don't fully understand the ramifications of yet, as you might be able to lift some of those restrictions.</div><div><br></div><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left-width:1px;border-left-color:rgb(204,204,204);border-left-style:solid;padding-left:1ex">
A little more thinking about this has led here: The distinction isn't really forall vs. pi. That is, in the cases where the levity matters, we don't really need to pi-quantify. Instead, it's exactly like type classes.<br></blockquote><div><br></div><div>In many ways pi comes down to doing typeclass like things, you're tracking information from the type system. The vehicle we have for doing that today is typeclasses. I've been thinking about anything that i have that actually needs the "pi" there as a form of "constraint" passing all along, with the constraint being whatever introspection you need to allow on the type to carry on.</div><div><br></div><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left-width:1px;border-left-color:rgb(204,204,204);border-left-style:solid;padding-left:1ex">
Imagine, for a moment, that we have an alternate universe where strict is the default, and we have<br>
<br>
> data Lazy a = Thunk (() -> a) | WHNF a<br>
<br>
The WHNF is a bit of a lie, because this representation would mean that the contents of a WHNF are fully evaluated. But let's not get hung up on that point.<br>
<br>
Then, we have<br>
<br>
> type family BaseType a where<br>
> BaseType (Lazy a) = a<br>
> BaseType a = a<br>
><br>
> class Forceable a where<br>
> force :: a -> BaseType a<br>
><br>
> instance Forceable a where<br>
> force = id<br>
><br>
> instance Forceable (Lazy a) where<br>
> force (Thunk f) = f ()<br>
> force (WHNF a) = a<br>
<br>
Things that need to behave differently depending on strictness just take a dictionary of the Forceable class. Equivalently, they make a runtime decision of whether to force or not. So we don't need an exponential number of maps. We need a map that makes some runtime decisions. And the optimizer can be taught that specializing these decisions may be helpful.<br>
<br>
Of course, none of this would be exposed. And I'm not suggesting that we need to make the core language strict-by-default. But it clarified things, for me at least, when I realized this is regular old ad-hoc polymorphism, not something fancier.</blockquote><div><br></div><div>Yep. </div><div><br></div><div>-Edward</div></div></div></div>