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

[prev in list] [next in list] [prev in thread] [next in thread] 

List:       haskell-cafe
Subject:    [Haskell-cafe] Explicit type signatures and wrappers / impedance-matching
From:       Benjamin Redelings <benjamin.redelings () gmail ! com>
Date:       2022-01-31 22:50:57
Message-ID: 69bf561f-2fea-d1dd-4485-75e7dcbe28de () gmail ! com
[Download RAW message or body]

[Attachment #2 (multipart/alternative)]

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

[Attachment #5 (text/html)]

<html>
  <head>

    <meta http-equiv="content-type" content="text/html; charset=UTF-8">
  </head>
  <body>
    <p>Hi,</p>
    <p>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>
    </p>
    <p>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>
    </p>
    <p>2. Do explicit type signatures impose any unification
      constraints, or can they be thought of entirely in terms of
      wrappers?</p>
    <p>For example, if we have <br>
    </p>
    <pre>g :: Int -&gt; Int
(f,g) = (\x -&gt;x, f)
</pre>
    <p>then the signature for g is added to the environment when typing
      the right-hand-side.</p>
    <p>One way that this could be handled is:</p>
    <p>(i) typecheck rhs -&gt; rhs_type<br>
    </p>
    <p>(ii) generate type of lhs with fresh variables for every binder
      -&gt; lhs_type = (a,b)<br>
    </p>
    <p>(iii) unify(lhs_type, rhs_type)</p>
    <p>(iv) do one-way unification: match(inferred-type-of-g,
      explicit-type-for-g)</p>
    <p>Is this correct?  Step (iv), the way that I have written it,
      would impose unification constraints.</p>
    <p>Without considering the type signature, we would have</p>
    <p>{ f_mono :: a -&gt; a, g_mono :: a -&gt; a}</p>
    <p>If we just use wrappers to impose the explict type, it seems like
      we would get something like<br>
    </p>
    <pre>let tup = /\a.let {(f:a,g:a) = (\x:a -&gt; x:a, f::a-&gt;a)
    f = /\a.case tup a of (f,g) -&gt; f
    g = case tup @Int of (f,g) -&gt; g

</pre>
    <p>where f :: forall a.a -&gt;a and g :: Int -&gt; Int.</p>
    <p>THIH seems to imply that type signatures are merely checked: no
      unification constraints are imposed (I think).  However, ghc
      reports f :: Int -&gt; Int.</p>
    <p>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>thanks!<br>
    </p>
    <p>-BenRI<br>
    </p>
  </body>
</html>

[Attachment #6 (text/plain)]

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

[prev in list] [next in list] [prev in thread] [next in thread] 