[Haskell-cafe] Explicit type signatures and wrappers / impedance-matching

[Benjamin Redelings]

Hi Richard,

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.

Here is my understanding so far -- please chime in if anything is 
obviously wrong here:

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.

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.

Then, for each binding, we end up with two different types:

1. The more quantified type for each binder

     forall qtvs. theta => monotype

This is what we get if we include ALL the type variables and ALL the 
predicates that will end up in the AbsBinds.

2. The actual type for each binder, that includes only SOME of the type 
variables and SOME of the predicates.

This is given either by

2a: an explicit type signature

2b: selecting some of the type variables some_qtvs and predicates 
some_predicates in chooseInferredQuantifiers.  We'd end up with

     forall some_qtvs. some_predicates => monotype

For example, if we have (f,g) = (\x->x, \y->y+2), then we don't want

     f :: forall a b.Num b => a -> a

we just want

     f :: a -> a

The first type is the more quantified type, and the second type is the 
actual type.

Then, in order to handle the difference between these two types, we call 
`tcSubTypeSigma actual_type more_quantified_type`, which

(i) checks to see that we can get `actual_type` out of 
`more_quantified_type` by constraining it somehow.

(i) returns an HsWrapper that, does the actually constraining.

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.


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.

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:

tuple = /\a./\b.\(dNum :: Num b). let ...CODE... in (f,g)

f' = /\a./\b.\(dNum :: b). case (tuple @a @b dNum) of f

f = /\a. f' @a @ANY dNum = apply wrapper to f' ?

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.


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:

f:: forall a.Num a -> a->a->a

(f,g) = ...rhs...

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...


Anyway, thanks for the encouragement.  I am not stuck, yet...

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.

-BenRI


[1] Determined in tcPolyInfer by calling simpliferInfer

On 2/15/22 4:49 PM, Richard Eisenberg wrote:
> Some time has passed. Have you made forward progress?
>
> 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!)
>
> 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.
>
> You seem to be doing interesting work -- please don't let yourself get 
> stuck. Keeping asking for answers if you need them! :)
>
> Richard
>
>> On Feb 7, 2022, at 8:21 PM, Benjamin Redelings 
>> <benjamin.redelings at gmail.com> wrote:
>>
>> 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.
>>
>> -BenRI
>>
>> On 1/31/22 2:50 PM, Benjamin Redelings wrote:
>>>
>>> Hi,
>>>
>>> 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.
>>>
>>> 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...
>>>
>>> 2. Do explicit type signatures impose any unification constraints, 
>>> or can they be thought of entirely in terms of wrappers?
>>>
>>> For example, if we have
>>>
>>> g :: Int -> Int
>>> (f,g) = (\x ->x, f)
>>>
>>> then the signature for g is added to the environment when typing the 
>>> right-hand-side.
>>>
>>> One way that this could be handled is:
>>>
>>> (i) typecheck rhs -> rhs_type
>>>
>>> (ii) generate type of lhs with fresh variables for every binder -> 
>>> lhs_type = (a,b)
>>>
>>> (iii) unify(lhs_type, rhs_type)
>>>
>>> (iv) do one-way unification: match(inferred-type-of-g, 
>>> explicit-type-for-g)
>>>
>>> Is this correct?  Step (iv), the way that I have written it, would 
>>> impose unification constraints.
>>>
>>> Without considering the type signature, we would have
>>>
>>> { f_mono :: a -> a, g_mono :: a -> a}
>>>
>>> If we just use wrappers to impose the explict type, it seems like we 
>>> would get something like
>>>
>>> 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
>>>
>>> where f :: forall a.a ->a and g :: Int -> Int.
>>>
>>> THIH seems to imply that type signatures are merely checked: no 
>>> unification constraints are imposed (I think).  However, ghc reports 
>>> f :: Int -> Int.
>>>
>>> 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.
>>>
>>> thanks!
>>>
>>> -BenRI
>>>
>> _______________________________________________
>> Haskell-Cafe mailing list
>> To (un)subscribe, modify options or view archives go to:
>> http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
>> Only members subscribed via the mailman list are allowed to post.
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/haskell-cafe/attachments/20220222/caea708c/attachment.html>