I've been a bit under water of late, so I haven't gotten to respond to this.
But is this superseded by your later email? If not, I'm happy to take a stab at
an answer.
Thanks,
Richard
> On Jan 15, 2022, at 2:09 PM, Benjamin Redelings
> <benjamin.redeli...@gmail.com> wrote:
>
> Hi,
>
> 1. I'm reading "A Static semantics for Haskell" and trying to code it up. I
> came across some odd behavior with pattern bindings, and I was wondering if
> someone could explain or point me in the right direction.
>
> Suppose you have the declaration
>
> (x,y) = ('a',2)
>
> My current code is yielding:
>
> x :: Num a => Char
>
> y :: Num a => a
>
> However, I notice that ghci gives x the type Char, with no constraint, which
> is what I would expect. It also gives y the type 'Num b => b', so I don't
> think it is defaulting a to Int here.
>
> The weird results from my code stem from rule BIND-PRED in Figure 15 of
> https://homepages.inf.ed.ac.uk/wadler/papers/staticsemantics/static-semantics.ps
>
> E |- bind ~~> \dicts : theta -> monobinds in bind : (LIE_{encl}, theta
> => LVE)
>
> Here theta = ( Num a ) and LVE = { x :: Char, y :: a }. So, theta => LVE is
>
> { x :: Num a => Char, y :: Num a => a }
>
> The obvious thing to do is avoid changing a type T to Num a => T if T does
> not contain a. Also I'm not totally sure if that trick gets to the bottom of
> the issue. However, the paper doesn't mention define theta => LVE that way.
> Is there something else I should read on this?
>
> 2. If we just chop out predicates which mention variables not in the type (
> == ambiguous predicates?) then I'm not totally sure how to create code for
> this.
>
> I would imagine that we have something like
>
> tup dn = ('a', fromInteger dn 2)
>
> x = case (tup dn) of (x,y) -> x
>
> y dn case (tup dn) of (x,y) -> y
>
> In this case its not clear where to get the `dn` argument of `tup` from, in
> the definition of `x`. Can we pass in `undefined`? Should we do something
> else?
>
> If anyone can shed light on this, I would be grateful :-)
>
> -BenRI
>
> _______________________________________________
> ghc-devs mailing list
> ghc-devs@haskell.org
> http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs
_______________________________________________
ghc-devs mailing list
ghc-devs@haskell.org
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs
