<html>
<head>
<meta http-equiv="Content-Type" content="text/html; charset=UTF-8">
</head>
<body>
<p>Hi Richard,</p>
<p>Thanks for asking! Yes, I'm making forward progress. The
feedback is appreciated, as I am not always sure which things I am
struggling with are silly questions and which ones are hard
questions.<br>
</p>
<p>Here is my understanding so far -- please chime in if anything is
obviously wrong here:<br>
</p>
<p>I. So, an AbsBinds contains a collection of bindings that could
be mutually recursive. It has constraints "theta" and quantifies
over type variables "qtvs" [1]. It also contains "evidence
bindings" that explain how to construct dictionaries that are
needed from dictionary arguments.<br>
</p>
<p>An AbsBinds can contain multiple bindings, for example if we have
two mutually recursive functions with no type signatures.
However, a recursive group can be split into multiple separate
AbsBinds if type signatures allow breaking some of the
dependencies. Each binding inside the AbsBinds has a type
"monotype" (from tcMonoBinds) before we generalize.</p>
<p>Then, for each binding, we end up with two different types:<br>
</p>
<p>1. The more quantified type for each binder</p>
<p> forall qtvs. theta => monotype</p>
<p>This is what we get if we include ALL the type variables and ALL
the predicates that will end up in the AbsBinds.</p>
<p>2. The actual type for each binder, that includes only SOME of
the type variables and SOME of the predicates.</p>
<p>This is given either by</p>
<p>2a: an explicit type signature <br>
</p>
<p>2b: selecting some of the type variables some_qtvs and predicates
some_predicates in chooseInferredQuantifiers. We'd end up with <br>
</p>
<p> forall some_qtvs. some_predicates => monotype<br>
</p>
<p>For example, if we have (f,g) = (\x->x, \y->y+2), then we
don't want <br>
</p>
<p> f :: forall a b.Num b => a -> a</p>
<p>we just want <br>
</p>
<p> f :: a -> a<br>
</p>
<p>The first type is the more quantified type, and the second type
is the actual type.<br>
</p>
<p>Then, in order to handle the difference between these two types,
we call `tcSubTypeSigma actual_type more_quantified_type`, which<br>
</p>
<p>(i) checks to see that we can get `actual_type` out of
`more_quantified_type` by constraining it somehow.<br>
</p>
<p>(i) returns an HsWrapper that, does the actually constraining. </p>
<p>It may (I think) eliminate predicates by defaulting, and it can
eliminate types by substituting an ANY type, at least sometimes.
This wrapper is stored inside abe_wrap field of ABE objects,
inside the abs_exports field of the AbsBinds.<br>
</p>
<p><br>
</p>
<p>II. I am still not completely sure how the wrapper is actually
applied in code generation, or how the wrapper is computed from
the two types. But, I'm not quite done reading yet.<br>
</p>
<p>For example, in the case above, suppose that `tuple` represents
all combined binders inside the AbsBinds, and is quantified by ALL
the type variables and ALL the (given) dictionaries. One approach
would be something like:<br>
</p>
<p>tuple = /\a./\b.\(dNum :: Num b). let ...CODE... in (f,g)<br>
</p>
<p>f' = /\a./\b.\(dNum :: b). case (tuple @a @b dNum) of f<br>
</p>
<p>f = /\a. f' @a @ANY dNum = apply wrapper to f' ?<br>
</p>
<p>In that approach, then we would FIRST extract an "f'" from the
tuple without applying any wrapper. Then, SECOND, we would SECOND
apply the wrapper to f' to get f.</p>
<p><br>
</p>
<p>III. I am also still working through tcMonoBinds. I'm curious
what happens in a pattern binding, when the pattern has a type
signature with predicates:</p>
<p>f:: forall a.Num a -> a->a->a</p>
<p>(f,g) = ...rhs...</p>
<p>It looks like the type signature for gets instantiated on the
LHS, and.... I presume the predicate Num a is added to the local
instance environment, just like if f was instantiated on the
RHS? I will think about this more...<br>
</p>
<p><br>
</p>
<p>Anyway, thanks for the encouragement. I am not stuck, yet...</p>
<p>All this does make me think that, perhaps, some kind of updated
version of Typing Haskell in Haskell would be appropriate. I'm
not sure how much of this is in the Report, either.<br>
</p>
<p>-BenRI<br>
</p>
<p><br>
</p>
<p>[1] Determined in tcPolyInfer by calling simpliferInfer<br>
</p>
<div class="moz-cite-prefix">On 2/15/22 4:49 PM, Richard Eisenberg
wrote:<br>
</div>
<blockquote type="cite"
cite="mid:010f017eff5d1ae7-74e6accb-7e6c-45a8-8096-33fe9d9e64c3-000000@us-east-2.amazonses.com">
<meta http-equiv="Content-Type" content="text/html; charset=UTF-8">
Some time has passed. Have you made forward progress?
<div class=""><br class="">
</div>
<div class="">The truth is that the particular case you describe
would make me, too, stare hard at the code. (This is why I have
been slow to respond!)</div>
<div class=""><br class="">
</div>
<div class="">One thing I can say is that I do not think
HsWrappers are much implicated. They are involved with
instantiation of type variables and of dictionaries (among other
fun things). Instead, look for a construct called AbsBinds,
which is heavily implicated here.</div>
<div class=""><br class="">
</div>
<div class="">You seem to be doing interesting work -- please
don't let yourself get stuck. Keeping asking for answers if you
need them! :)</div>
<div class=""><br class="">
</div>
<div class="">Richard<br class="">
<div><br class="">
<blockquote type="cite" class="">
<div class="">On Feb 7, 2022, at 8:21 PM, Benjamin Redelings
<<a href="mailto:benjamin.redelings@gmail.com"
class="moz-txt-link-freetext" moz-do-not-send="true">benjamin.redelings@gmail.com</a>>
wrote:</div>
<br class="Apple-interchange-newline">
<div class="">
<meta http-equiv="Content-Type" content="text/html;
charset=UTF-8" class="">
<div class="">
<p class="">So... I suspect that the best way forwards
is just to read GHC/TC/Gen/Bind.hs and make notes on
all the functions. That is what I am doing.<br
class="">
</p>
<p class="">-BenRI<br class="">
</p>
<div class="moz-cite-prefix">On 1/31/22 2:50 PM,
Benjamin Redelings wrote:<br class="">
</div>
<blockquote type="cite"
cite="mid:69bf561f-2fea-d1dd-4485-75e7dcbe28de@gmail.com"
class="">
<meta http-equiv="content-type" content="text/html;
charset=UTF-8" class="">
<p class="">Hi,</p>
<p class="">I am trying to understand (and implement)
how Haskell handles explicit type signatures.
Specifically, I'm trying to understand how explicit
type signatures interact with wrappers. <br
class="">
</p>
<p class="">1. Is there any paper or documentation
that explains wrappers and/or explicit type
signatures in detail? There are some non-obvious
details regarding wrappers, such as using
eliminating type arguments by supplying the Any type
as an argument...<br class="">
</p>
<p class="">2. Do explicit type signatures impose any
unification constraints, or can they be thought of
entirely in terms of wrappers?</p>
<p class="">For example, if we have <br class="">
</p>
<pre class="">g :: Int -> Int
(f,g) = (\x ->x, f)
</pre>
<p class="">then the signature for g is added to the
environment when typing the right-hand-side.</p>
<p class="">One way that this could be handled is:</p>
<p class="">(i) typecheck rhs -> rhs_type<br
class="">
</p>
<p class="">(ii) generate type of lhs with fresh
variables for every binder -> lhs_type = (a,b)<br
class="">
</p>
<p class="">(iii) unify(lhs_type, rhs_type)</p>
<p class="">(iv) do one-way unification:
match(inferred-type-of-g, explicit-type-for-g)</p>
<p class="">Is this correct? Step (iv), the way that
I have written it, would impose unification
constraints.</p>
<p class="">Without considering the type signature, we
would have</p>
<p class="">{ f_mono :: a -> a, g_mono :: a ->
a}</p>
<p class="">If we just use wrappers to impose the
explict type, it seems like we would get something
like<br class="">
</p>
<pre class="">let tup = /\a.let {(f:a,g:a) = (\x:a -> x:a, f::a->a)
f = /\a.case tup a of (f,g) -> f
g = case tup @Int of (f,g) -> g
</pre>
<p class="">where f :: forall a.a ->a and g :: Int
-> Int.</p>
<p class="">THIH seems to imply that type signatures
are merely checked: no unification constraints are
imposed (I think). However, ghc reports f :: Int
-> Int.</p>
<p class="">I apologize if this is a dumb question. I
have found the definition of HsWrapper in
ghc/compiler/GHC/Tc/Types/Evidence.hs, but I am
still struggling a bit.</p>
<p class="">thanks!<br class="">
</p>
<p class="">-BenRI<br class="">
</p>
</blockquote>
</div>
_______________________________________________<br
class="">
Haskell-Cafe mailing list<br class="">
To (un)subscribe, modify options or view archives go to:<br
class="">
<a
href="http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe"
class="moz-txt-link-freetext" moz-do-not-send="true">http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe</a><br
class="">
Only members subscribed via the mailman list are allowed
to post.</div>
</blockquote>
</div>
<br class="">
</div>
</blockquote>
</body>
</html>