Re: Type inference of singular matches on GADTs
i like how you've boiled down this discussion, it makes it much clearer to me at least :) On Sun, Mar 28, 2021 at 10:19 PM Richard Eisenberg wrote: > > > 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 > ___ > 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
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___ ghc-devs mailing list ghc-devs@haskell.org http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs
Re: Options for targeting Windows XP?
Hi all, only want to add a small note: there was (is?) a ghc fork targeting the jvm where i had the luck to been able to contribute my two cents: eta-lang (https://github.com/typelead/eta) Unfortunately the startup behind it lost funds and it is stalled but i still have the hope some day can be resurrected. Javi Neira El vie., 26 mar. 2021 10:42, Simon Peyton Jones via ghc-devs < ghc-devs@haskell.org> escribió: > This link gives some (old) background > > > https://wiki.haskell.org/GHC/FAQ#Why_isn.27t_GHC_available_for_.NET_or_on_the_JVM.3F > > Simon > > > > *From:* ghc-devs *On Behalf Of *Moritz > Angermann > *Sent:* 26 March 2021 08:00 > *To:* Clinton Mead > *Cc:* ghc-devs > *Subject:* Re: Options for targeting Windows XP? > > > > I believe there is a bit of misconception about what requires a new > backend or not. GHC is a bunch of different intermediate representations > from which one can take off to build backends. The STG, or Cmm ones are the > most popular. All our Native Code Generators and the LLVM code gen take off > from the Cmm one. Whether or not that is the correct input representation > for your target largely depends on the target and design of the > codegenerator. GHCJS takes off from STG, and so does Csaba's GRIN work via > the external STG I believe. IIRC Asterius takes off from Cmm. I don't > remember the details about Eta. > > > > Why fork? Do you want to deal with GHC, and GHC's development? If not, > fork. Do you want to have to keep up with GHC's development? Maybe not > fork. Do you think your compiler can stand on it's own and doesn't follow > GHC much, except for being a haskell compiler? By all means fork. > > > > Eta is a bit special here, Eta forked off, and basically started > customising their Haskell compiler specifically to the JVM, and this also > allowed them to make radical changes to GHC, which would not have been > permissible in the mainline GHC. (Mainline GHC tries to support multiple > platforms and architectures at all times, breaking any of them isn't really > an option that can be taken lightheartedly.) Eta also started having Etlas, > a custom Cabal, ... I'd still like to see a lot from Eta and the ecosystem > be re-integrated into GHC. There have to be good ideas there that can be > brought back. It just needs someone to go look and do the work. > > > > GHCJS is being aligned more with GHC right now precisely to eventually > re-integrate it with GHC. > > > > Asterius went down the same path, likely inspired by GHCJS, but I think I > was able to convince the author that eventual upstreaming should be the > goal and the project should try to stay as close as possible to GHC for > that reason. > > > > Now if you consider adding a codegen backend, this can be done, but again > depends on your exact target. I'd love to see a CLR target, yet I don't > know enough about CLR to give informed suggestions here. > > > > If you have a toolchain that functions sufficiently similar to a stock c > toolchain, (or you can make your toolchain look sufficiently similar to > one, easily), most of it will just work. If you can separate your building > into compilation of source to some form of object code, and some form of > object code aggregates (archives), and some form of linking (objects and > archives into shared objects, or executables), you can likely plug in your > toolchain into GHC (and Cabal), and have it work, once you taught GHC how > to produce your target languages object code. > > > > If your toolchain does stuff differently, a bit more work is involved in > teaching GHC (and Cabal) about that. > > > > This all only gives you *haskell* though. You still need the Runtime > System. If you have a C -> Target compiler, you can try to re-use GHC's > RTS. This is what the WebGHC project did. They re-used GHC's RTS, and > implemented a shim for linux syscalls, so that they can emulate enough to > have the RTS think it's running on some musl like linux. You most likely > want something proper here eventually; but this might be a first stab at it > to get something working. > > > > Next you'll have to deal with c-bits. Haskell Packages that link against C > parts. This is going to be challenging, not impossible but challenging as > much of the haskell ecosystem expects the ability to compile C files and > use those for low level system interaction. > > > > You can use hackage overlays to build a set of patched packages, once you > have your codegen working. At that point you could start patching ecosystem > packages to work on your target, until your changes are upstreamed, and > provide your user with a hackage overlay (essentially hackage + patches for > specific packages). > > > > Hope this helps. > > > > You'll find most of us on irc.freenode.net#ghc >
Re: Type inference of singular matches on GADTs
Hi Alexis,
If you really want to get by without type annotations, then Viktor's
pattern synonym suggestion really is your best option! Note that
pattern HNil :: HList '[];
pattern HNil = HNil_
Does not actually declare an HNil that is completely synonymous with HNil_,
but it changes the *provided* GADT constraint (as ~ '[]) into a *required*
constraint (as ~ '[]).
"Provided" as in "a pattern match on the synonym provides this constraint
as a new Given", "required" as in "... requires this constraint as a new
Wanted". (I hope I used the terminology correctly here.)
Thus, a pattern ((a :: Int) `HCons` HNil) really has type (HList '[Int])
and is exhaustive. See also
https://gitlab.haskell.org/ghc/ghc/-/wikis/pattern-synonyms#static-semantics
.
At the moment, I don't think it's possible to declare a GADT constructor
with required constraints, so a pattern synonym seems like your best bet
and fits your use case exactly.
You can put each of these pattern synonyms into a singleton COMPLETE pragma.
Hope that helps,
Sebastian
Am Sa., 27. März 2021 um 06:27 Uhr schrieb Viktor Dukhovni <
ietf-d...@dukhovni.org>:
> On Fri, Mar 26, 2021 at 07:41:09PM -0500, Alexis King wrote:
>
> > type applications in patterns are still not enough to satisfy me. I
> > provided the empty argument list example because it was simple, but I’d
> > also like this to typecheck:
> >
> > baz :: Int -> String -> Widget
> > baz =
> >
> > bar = foo (\(a `HCons` b `HCons` HNil) -> baz a b)
> >
>
> Can you be a bit more specific on how the constraint `Blah` is presently
> defined, and how `foo` uses the HList type to execute a function of the
> appropriate arity and signature?
>
> The example below my signature typechecks, provided I use pattern
> synonyms for the GADT constructors, rather than use the constructors
> directly.
>
> --
> Viktor.
>
> {-# language DataKinds
>, FlexibleInstances
>, GADTs
>, PatternSynonyms
>, ScopedTypeVariables
>, TypeApplications
>, TypeFamilies
>, TypeOperators
>#-}
>
> import GHC.Types
> import Data.Proxy
> import Type.Reflection
> import Data.Type.Equality
>
> data HList as where
> HNil_ :: HList '[]
> HCons_ :: a -> HList as -> HList (a ': as)
> infixr 5 `HCons_`
>
> pattern HNil :: HList '[];
> pattern HNil = HNil_
> pattern (:^) :: a -> HList as -> HList (a ': as)
> pattern (:^) a as = HCons_ a as
> pattern (:$) a b = a :^ b :^ HNil
> infixr 5 :^
> infixr 5 :$
>
> class Typeable as => Blah as where
> params :: HList as
> instance Blah '[Int,String] where
> params = 39 :$ "abc"
>
> baz :: Int -> String -> Int
> baz i s = i + length s
>
> bar = foo (\(a :$ b) -> baz a b)
>
> foo :: Blah as => (HList as -> Int) -> Int
> foo f = f params
> ___
> 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
Re: Pattern matching desugaring regression? Re: [Haskell-cafe] Why does my module take so long to compile?
Hi Troels,
Sorry to hear GHC 9 didn't fix your problems! Yes, please open an issue.
Optimising for specific usage patterns might be feasible, although note
that most often it's not the exhaustivity check that is causing problems,
but the check for overlapping patterns.
At the moment the checker doesn't take shortcuts if we have
-Wincomplete-patterns, but -Wno-overlapping-patterns. Maybe it could? Let's
see what is causing you problems and decide then.
Cheers,
Sebastian
Am So., 28. März 2021 um 15:44 Uhr schrieb Troels Henriksen <
at...@sigkill.dk>:
> Troels Henriksen writes:
>
> > It is very likely that issue 17386 is the issue. With
> >
> > {-# OPTIONS_GHC -Wno-overlapping-patterns -Wno-incomplete-patterns
> > -Wno-incomplete-uni-patterns -Wno-incomplete-record-updates #-}
> >
> > my module(s) compile very quickly. I'll wait and see if GHC 9 does
> > better before I try to create a smaller case (and now I at least have a
> > workaround).
>
> I have now tried it with GHC 9, and unfortunately it is still very slow.
>
> As time permits, I will see if I can come up with a self-contained
> module that illustrates the slowdown.
>
> I do have an idea for a optimisation: In all of the cases where coverage
> tracking takes a long time, I have a catch-all case at the bottom. I
> think that is a fairly common pattern, where a program tries to detect
> various special cases, before falling back to a general case. Perhaps
> coverage checking should have a short-circuiting check for whether there
> is an obvious catch-all case, and if so, not bother looking any closer?
>
> --
> \ Troels
> /\ Henriksen
>
___
ghc-devs mailing list
ghc-devs@haskell.org
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs
Re: Pattern matching desugaring regression? Re: [Haskell-cafe] Why does my module take so long to compile?
Troels Henriksen writes:
> It is very likely that issue 17386 is the issue. With
>
> {-# OPTIONS_GHC -Wno-overlapping-patterns -Wno-incomplete-patterns
> -Wno-incomplete-uni-patterns -Wno-incomplete-record-updates #-}
>
> my module(s) compile very quickly. I'll wait and see if GHC 9 does
> better before I try to create a smaller case (and now I at least have a
> workaround).
I have now tried it with GHC 9, and unfortunately it is still very slow.
As time permits, I will see if I can come up with a self-contained
module that illustrates the slowdown.
I do have an idea for a optimisation: In all of the cases where coverage
tracking takes a long time, I have a catch-all case at the bottom. I
think that is a fairly common pattern, where a program tries to detect
various special cases, before falling back to a general case. Perhaps
coverage checking should have a short-circuiting check for whether there
is an obvious catch-all case, and if so, not bother looking any closer?
--
\ Troels
/\ Henriksen
___
ghc-devs mailing list
ghc-devs@haskell.org
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs
