Re: Type inference of singular matches on GADTs

[Richard Eisenberg]

As usual, I want to separate out the specification of a feature from the 
implementation. So let's just focus on specification for now -- with the caveat 
that there might be no possible implementation of these ideas.

The key innovation I see lurking here is the idea of an *exhaustive* function, 
where we know that any pattern-match on an argument is always exhaustive. I 
will write such a thing with @->, in both the type and in the arrow that 
appears after the lambda. The @-> type is a subtype of -> (and perhaps does not 
need to be written differently from ->).

EX1: \x @-> case x of HNil -> blah

This is easy: we can infer HList '[] @-> blah's type, because the pattern match 
is declared to be exhaustive, and no other type grants that property.

EX2: \x @-> (x, case x of HNit -> blah)

Same as EX1.

EX3: \x @-> case x of { HNil1 -> blah; HNil2 -> blah }

Same as EX1. There is still a unique type for which the patten-match is 
exhaustive.

EX4: Reject. There are multiple valid types, and we don't know which one to 
pick. This is like classic untouchable-variables territory.

EX5: This is hard. A declarative spec would probably choose HL2 [a] -> ... as 
you suggest, but there may be no implementation of such an idea.

EX6: Reject. No type leads to exhaustive matches.

I'm not saying this is a good idea for GHC or that it's implementable. But the 
idea of having type inference account for exhaustivity in this way does not 
seem, a priori, unspecified.

Richard



> On Mar 29, 2021, at 5:00 AM, Simon Peyton Jones  wrote:
> 
> I haven't thought about how to implement such a thing. At the least, it would 
> probably require some annotation saying that we expect `\HNil -> ()` to be 
> exhaustive (as GHC won't, in general, make that assumption). Even with that, 
> could we get type inference to behave? Possibly.
>  
> As I wrote in another post on this thread, it’s a bit tricky. 
>  
> What would you expect of (EX1)
>  
>\x -> case x of HNil -> blah
>  
> Here the lambda and the case are separated
>  
> Now (EX2)
>  
> \x -> (x, case x of HNil -> blah)
>  
> Here the lambda and the case are separated more, and x is used twice.
> What if there are more data constructors that share a common return type? 
> (EX3)
>  
> data HL2 a where
> HNil1 :: HL2 []
> HNil2 :: HL2 []
> HCons :: …blah…
>  
> \x -> case x of { HNil1 -> blah; HNil 2 -> blah  }
>  
> Here HNil1 and HNil2 both return HL2 [].   Is that “singular”?   
>  
> What if one was a bit more general than the other?   Do we seek the least 
> common generalisation of the alternatives given? (EX4)
>  
> data HL3 a where
> HNil1 :: HL2 [Int]
> HNil2 :: HL2 [a]
> HCons :: …blah…
>  
> \x -> case x of { HNil1 -> blah; HNil 2 -> blah  }
>  
> What if the cases were incompatible?  (EX5)
>  
> data HL4 a where
> HNil1 :: HL2 [Int]
> HNil2 :: HL2 [Bool]
> HCons :: …blah…
>  
> \x -> case x of { HNil1 -> blah; HNil 2 -> blah  }
>  
> Would you expect that to somehow generalise to `HL4 [a] -> blah`?
> 
> What if x matched multiple times, perhaps on different constructors (EX6)
> 
> \x -> (case s of HNil1 -> blah1;  case x of HNil2 -> blah)
>  
>  
> The water gets deep quickly here.  I don’t (yet) see an obviously-satisfying 
> design point that isn’t massively ad-hoc.
>  
> Simon
>  
>  
> From: ghc-devs  On Behalf Of Richard Eisenberg
> Sent: 29 March 2021 03:18
> To: Alexis King 
> Cc: ghc-devs@haskell.org
> Subject: Re: Type inference of singular matches on GADTs
>  
>  
> 
> 
> On Mar 26, 2021, at 8:41 PM, Alexis King  > wrote:
>  
> If there’s a single principal type that makes my function well-typed and 
> exhaustive, I’d really like GHC to pick it.
>  
> I think this is the key part of Alexis's plea: that the type checker take 
> into account exhaustivity in choosing how to proceed.
>  
> Another way to think about this:
>  
> f1 :: HList '[] -> ()
> f1 HNil = ()
>  
> f2 :: HList as -> ()
> f2 HNil = ()
>  
> Both f1 and f2 are well typed definitions. In any usage site where both are 
> well-typed, they will behave the same. Yet f1 is exhaustive while f2 is not. 
> This isn't really about an open-world assumption or the possibility of extra 
> cases -- it has to do with what the runtime behaviors of the two functions 
> are. f1 never fails, while f2 must check a constructor tag and perhaps throw 
> an exception.
>  
> If we just see \HNil -> (), Alexis seems to be suggesting we prefer the f1 
> interpretation over the f2 interpretation. Why? Because f1 is exhaustive, and 
> when we can choose an exhaustive interpretation, that's probably a good idea 
> to pursue.
>  
> I haven't thought about how to implement such a thing. At the least, it would 
> probably require some annotation saying that we expect `\HNil -> ()` to be 
> exhaustive (as GHC won't, in general, make that assumption). Even with that, 
> could we get type inference to behave? Possibly.
>  
> But first: does this match your understanding?
>  
> Richard

Re: Options for targeting Windows XP?

[Moritz Angermann]

>
>* Upstream changes into Cabal to make your new compiler a first-class
>  citizen. This is what GHCJS did.


Just a word of caution, please don't do this. It leads to non-negligible
maintainence burden on your and on the cabal side. Rather try as hard as
you can to make your compiler behave like a ghc wrt to cabal. Or add
generic support for more powerful compilers to cabal. Adding special
handling for one additional compiler will just result in bitrot, odd quirks
that only happen with that one compiler, and just a maintenance nightmare
for everyone involved.

We will be ripping out GHCJS custom logic from cabal. And I've also advised
the Asterius author not to go down that route.

My suggesting--if I may--is to try and build a c-like toolchain around your
compiler. That has some notion of compiler, archiver, linker, and those
could you empty shell wrappers, or no-ops, depending on your target.

Cheers,
 Moritz

On Tue, Mar 30, 2021 at 11:08 AM Ben Gamari  wrote:

> Clinton Mead  writes:
>
> > Thanks again for the detailed reply Ben.
> >
> > I guess the other dream of mine is to give GHC a .NET backend. For my
> > problem it would be the ideal solution, but it looks like other attempts
> in
> > this regard (e.g. Eta, GHCJS etc) seem to have difficulty keeping up with
> > updates to GHC. So I'm sure it's not trivial.
> >
> > It would be quite lovely though if I could generate .NET + Java + even
> > Python bytecode from GHC.
> >
> > Whilst not solving my immediate problem, perhaps my efforts are best
> spent
> > in giving GHC a plugin architecture for backends (or if one already
> > exists?) trying to make a .NET backend.
> >
> This is an interesting (albeit ambitious, for the reasons others have
> mentioned) idea. In particular, I think the CLR has a slightly advantage
> over the JVM as a Haskell target in that it has native tail-call
> support [1]. This avoids a fair amount of complexity (and performance
> overhead) that Eta had to employ to work around this lack in the JVM.
>
> I suspect that writing an STG -> CLR IR wouldn't itself be difficult.
> The hard part is dealing with the primops, RTS, and core libraries.
>
> [1]
> https://docs.microsoft.com/en-us/previous-versions/windows/silverlight/dotnet-windows-silverlight/56c08k0k(v=vs.95)?redirectedfrom=MSDN
>
> > I believe "Csaba Hruska" is working in this space with GRIN, yes?
>
> Csaba is indeed using GHC's front-end and Core pipeline to feed his own
> compilation pipeline. However, I believe his approach is currently quite
> decoupled from GHC. This may or may not complicate the ability to
> integrate with the rest of the ecosystem (e.g. Cabal; Csaba, perhaps you
> could
> comment here?)
>
>
> >
> > I read SPJs paper on Implementing Lazy Functional Languages on Stock
> > Hardware: The Spineless Tagless G-machine
> > <
> https://www.microsoft.com/en-us/research/publication/implementing-lazy-functional-languages-on-stock-hardware-the-spineless-tagless-g-machine/
> >
> > which
> > implemented STG in C and whilst it wasn't trivial, it didn't seem
> > stupendously complex (even I managed to roughly follow it). I thought to
> > myself also, implementing this in .NET would be even easier because I can
> > hand off garbage collection to the .NET runtime so there's one less thing
> > to worry about. I also, initially, don't care _too_ much about
> performance.
> >
> Indeed, STG itself is reasonably straightforward. Implementing tagged
> unions in the CLR doesn't even look that hard (F# does it, afterall).
> However, there are plenty of tricky bits:
>
>  * You still need to implement a fair amount of RTS support for a full
>implementation (e.g. light-weight threads and STM)
>
>  * You need to shim-out or reimplement the event manager in `base`
>
>  * What do you do about the many `foreign import`s used by, e.g.,
>`text`?
>
>  * How do you deal with `foreign import`s elsewhere?
>
> > Of course, there's probably a whole bunch of nuance. One actually needs
> to,
> > for example, represent all the complexities of GADTs into object
> orientated
> > classes, maybe converting sum types to inheritance hierarchies with
> Visitor
> > Patterns. And also you'd actually have to make sure to do one's best to
> > ensure exposed Haskell functions look like something sensible.
> >
> > So I guess, given I have a bit of an interest here, what would be the
> best
> > approach if I wanted to help GHC develop more backends and into an
> > architecture where people can add backends without forking GHC? Where
> could
> > I start helping that effort? Should I contact "Csaba Hruska" and get
> > involved in GRIN? Or is there something that I can start working on in
> GHC
> > proper?
> >
> At the moment we rather lack a good model for how new backends should
> work. There are quite a few axes to consider here:
>
>  * How do core libraries (e.g. `text`) work? Various choices are:
>
>* Disregard the core libraries (along with most of Hackage) and just
>  take the 

Re: Options for targeting Windows XP?

[Ben Gamari]

Clinton Mead  writes:

> Thanks again for the detailed reply Ben.
>
> I guess the other dream of mine is to give GHC a .NET backend. For my
> problem it would be the ideal solution, but it looks like other attempts in
> this regard (e.g. Eta, GHCJS etc) seem to have difficulty keeping up with
> updates to GHC. So I'm sure it's not trivial.
>
> It would be quite lovely though if I could generate .NET + Java + even
> Python bytecode from GHC.
>
> Whilst not solving my immediate problem, perhaps my efforts are best spent
> in giving GHC a plugin architecture for backends (or if one already
> exists?) trying to make a .NET backend.
>
This is an interesting (albeit ambitious, for the reasons others have
mentioned) idea. In particular, I think the CLR has a slightly advantage
over the JVM as a Haskell target in that it has native tail-call
support [1]. This avoids a fair amount of complexity (and performance
overhead) that Eta had to employ to work around this lack in the JVM.

I suspect that writing an STG -> CLR IR wouldn't itself be difficult.
The hard part is dealing with the primops, RTS, and core libraries.

[1] 
https://docs.microsoft.com/en-us/previous-versions/windows/silverlight/dotnet-windows-silverlight/56c08k0k(v=vs.95)?redirectedfrom=MSDN

> I believe "Csaba Hruska" is working in this space with GRIN, yes?

Csaba is indeed using GHC's front-end and Core pipeline to feed his own
compilation pipeline. However, I believe his approach is currently quite
decoupled from GHC. This may or may not complicate the ability to
integrate with the rest of the ecosystem (e.g. Cabal; Csaba, perhaps you could
comment here?)


>
> I read SPJs paper on Implementing Lazy Functional Languages on Stock
> Hardware: The Spineless Tagless G-machine
> 
> which
> implemented STG in C and whilst it wasn't trivial, it didn't seem
> stupendously complex (even I managed to roughly follow it). I thought to
> myself also, implementing this in .NET would be even easier because I can
> hand off garbage collection to the .NET runtime so there's one less thing
> to worry about. I also, initially, don't care _too_ much about performance.
>
Indeed, STG itself is reasonably straightforward. Implementing tagged
unions in the CLR doesn't even look that hard (F# does it, afterall).
However, there are plenty of tricky bits:

 * You still need to implement a fair amount of RTS support for a full
   implementation (e.g. light-weight threads and STM)

 * You need to shim-out or reimplement the event manager in `base`

 * What do you do about the many `foreign import`s used by, e.g.,
   `text`?

 * How do you deal with `foreign import`s elsewhere?

> Of course, there's probably a whole bunch of nuance. One actually needs to,
> for example, represent all the complexities of GADTs into object orientated
> classes, maybe converting sum types to inheritance hierarchies with Visitor
> Patterns. And also you'd actually have to make sure to do one's best to
> ensure exposed Haskell functions look like something sensible.
>
> So I guess, given I have a bit of an interest here, what would be the best
> approach if I wanted to help GHC develop more backends and into an
> architecture where people can add backends without forking GHC? Where could
> I start helping that effort? Should I contact "Csaba Hruska" and get
> involved in GRIN? Or is there something that I can start working on in GHC
> proper?
>
At the moment we rather lack a good model for how new backends should
work. There are quite a few axes to consider here:

 * How do core libraries (e.g. `text`) work? Various choices are:

   * Disregard the core libraries (along with most of Hackage) and just
 take the Haskell language

   * Reimplement many of the core libraries in the target language (e.g.
 as done by GHCJS)

 * How does the compiler interact with the Haskell build toolchain (e.g.
   Cabal)? Choices are:

   * Disregard the Haskell build toolchain. My (possibly incorrect)
 understanding is this is what GRIN does.

   * Implement something that looks enough like GHC to fool Cabal.

   * Upstream changes into Cabal to make your new compiler a first-class
 citizen. This is what GHCJS did.

 * How does the backend interact with GHC? Choices:
  
   * The GRIN model: Run the GHC pipeline and serialise the resulting IR
 (in the case of GRIN, STG) to a file to be slurped up by another process

   * The Clash/GHCJS model: Implement the new compiler as an executable
 linking against the GHC API. 

   * The frontend plugin model: For many years now GHC has had support
 for "front-end plugins". This mechanism allows a plugin to
 fundamentally redefine what the GHC executable does (e.g.
 essentially adding a new "mode" to GHC, a la --interactive or
 --make). It's not impossible that one could use this to implement a

GHC 9.2 has branched

[Ben Gamari]

Hello everyone,

At this point the ghc-9.2 branch has officially branched off from master.
If there was anything you were holding back from `master`, feel free to
now send it off to Marge.

I'll be working on doing some release prep and pushing out an alpha in
the next few days. This alpha will very likely lack the new NCG (which
is still being worked on by Moritz) but otherwise should be functionally
complete.

Cheers,

- Ben


signature.asc
Description: PGP signature
___
ghc-devs mailing list
ghc-devs@haskell.org
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs

RE: Type inference of singular matches on GADTs

[Simon Peyton Jones via ghc-devs]

I haven't thought about how to implement such a thing. At the least, it would 
probably require some annotation saying that we expect `\HNil -> ()` to be 
exhaustive (as GHC won't, in general, make that assumption). Even with that, 
could we get type inference to behave? Possibly.

As I wrote in another post on this thread, it’s a bit tricky.

What would you expect of (EX1)

   \x -> case x of HNil -> blah

Here the lambda and the case are separated

Now (EX2)

\x -> (x, case x of HNil -> blah)

Here the lambda and the case are separated more, and x is used twice.
What if there are more data constructors that share a common return type? (EX3)


data HL2 a where

HNil1 :: HL2 []

HNil2 :: HL2 []

HCons :: …blah…

\x -> case x of { HNil1 -> blah; HNil 2 -> blah  }

Here HNil1 and HNil2 both return HL2 [].   Is that “singular”?

What if one was a bit more general than the other?   Do we seek the least 
common generalisation of the alternatives given? (EX4)

data HL3 a where

HNil1 :: HL2 [Int]

HNil2 :: HL2 [a]

HCons :: …blah…

\x -> case x of { HNil1 -> blah; HNil 2 -> blah  }

What if the cases were incompatible?  (EX5)

data HL4 a where

HNil1 :: HL2 [Int]

HNil2 :: HL2 [Bool]

HCons :: …blah…

\x -> case x of { HNil1 -> blah; HNil 2 -> blah  }

Would you expect that to somehow generalise to `HL4 [a] -> blah`?

What if x matched multiple times, perhaps on different constructors (EX6)

\x -> (case s of HNil1 -> blah1;  case x of HNil2 -> blah)


The water gets deep quickly here.  I don’t (yet) see an obviously-satisfying 
design point that isn’t massively ad-hoc.

Simon


From: ghc-devs  On Behalf Of Richard Eisenberg
Sent: 29 March 2021 03:18
To: Alexis King 
Cc: ghc-devs@haskell.org
Subject: Re: Type inference of singular matches on GADTs




On Mar 26, 2021, at 8:41 PM, Alexis King 
mailto:lexi.lam...@gmail.com>> wrote:

If there’s a single principal type that makes my function well-typed and 
exhaustive, I’d really like GHC to pick it.

I think this is the key part of Alexis's plea: that the type checker take into 
account exhaustivity in choosing how to proceed.

Another way to think about this:

f1 :: HList '[] -> ()
f1 HNil = ()

f2 :: HList as -> ()
f2 HNil = ()

Both f1 and f2 are well typed definitions. In any usage site where both are 
well-typed, they will behave the same. Yet f1 is exhaustive while f2 is not. 
This isn't really about an open-world assumption or the possibility of extra 
cases -- it has to do with what the runtime behaviors of the two functions are. 
f1 never fails, while f2 must check a constructor tag and perhaps throw an 
exception.

If we just see \HNil -> (), Alexis seems to be suggesting we prefer the f1 
interpretation over the f2 interpretation. Why? Because f1 is exhaustive, and 
when we can choose an exhaustive interpretation, that's probably a good idea to 
pursue.

I haven't thought about how to implement such a thing. At the least, it would 
probably require some annotation saying that we expect `\HNil -> ()` to be 
exhaustive (as GHC won't, in general, make that assumption). Even with that, 
could we get type inference to behave? Possibly.

But first: does this match your understanding?

Richard
___
ghc-devs mailing list
ghc-devs@haskell.org
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs

Re: Type inference of singular matches on GADTs

[Viktor Dukhovni]

On Sun, Mar 28, 2021 at 11:00:56PM -0400, Carter Schonwald wrote:

> On Sun, Mar 28, 2021 at 10:19 PM Richard Eisenberg  wrote:
>
> > I think this is the key part of Alexis's plea: that the type checker take
> > into account exhaustivity in choosing how to proceed.
> >
> > Another way to think about this:
> >
> > f1 :: HList '[] -> ()
> > f1 HNil = ()
> >
> > f2 :: HList as -> ()
> > f2 HNil = ()
> >
> > Both f1 and f2 are well typed definitions. In any usage site where both
> > are well-typed, they will behave the same. Yet f1 is exhaustive while f2 is
> > not. ...
>
> I like how you've boiled down this discussion, it makes it much clearer to
> me at least :)

+1.  Very much distills it for me too.  Thanks!

FWIW, I've since boiled down the pattern-synonym example to the below,
where I find the choices of ":^" and ":$" to be pleasantly mnemonic,
though "HSolo" is perhaps a bit too distracting...

{-# language DataKinds, FlexibleInstances, FlexibleContexts, GADTs
   , PatternSynonyms, TypeOperators #-}
{-# OPTIONS_GHC -Wno-type-defaults #-}
import Data.Reflection
import Data.Proxy

default (Int)

data HList as where
  HNil_  :: HList '[]
  HCons_ :: a -> HList as -> HList (a ': as)
infixr 5 `HCons_`

pattern HNil :: HList '[];
pattern HNil  = HNil_

pattern HSolo :: a -> HList '[a]
pattern HSolo a = a :^ HNil

pattern (:^) :: a -> HList as -> HList (a ': as)
pattern (:^) a as = HCons_ a as
infixr 5 :^

pattern (:$) :: a -> b -> HList '[a,b]
pattern (:$) a b = a :^ HSolo b
infixr 5 :$

hApp :: Reifies s (HList as) => (HList as -> r) -> Proxy s -> r
hApp f = f . reflect

main :: IO ()
main = do
print $ reify HNil  $ hApp (\ HNil -> 42)
print $ reify (HSolo42) $ hApp (\ (HSolo a) -> a)
print $ reify (28 :$ "0xe") $ hApp (\ (a :$ b) -> a + read b)

-- 
Viktor.
___
ghc-devs mailing list
ghc-devs@haskell.org
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs