On 3/28/21 9:17 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.
[…]
Does this match your understanding?
Yes, precisely. :) Without GADTs, exhaustivity doesn’t yield any useful
inf
soning. I can’t yet see how to write a formal
specification. Note “yet” -- growth mindset!
Simon
From: Richard Eisenberg
Sent: 30 March 2021 04:58
To: Simon Peyton Jones
Cc: Alexis King ; ghc-devs@haskell.org
Subject: Re: Type inference of singular matches on GADTs
As usual, I want to separa
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.
>
>
lah1; 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
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 abou
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*,
> 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
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 *provide
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 =
>
I appreciate your point Sebastian, but I think in this particular case,
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 =
b
Cale made me aware of the fact that the "Type applications in patterns"
proposal had already been implemented.
See https://gitlab.haskell.org/ghc/ghc/-/issues/19577 where I adapt Alexis'
use case into a test case that I'd like to see compiling.
Am Sa., 20. März 2021 um 15:45 Uhr schrieb Sebastian
generalisation of the alternatives given?
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 Alexis King
Sent: 20 March 2021 09:41
To: ghc-devs@haskell.org
Subject: Type inference of singular matc
Hi Alexis,
The following works and will have inferred type `Int`:
> bar = foo (\(HNil :: HList '[]) -> 42)
I'd really like it if we could write
> bar2 = foo (\(HNil @'[]) -> 42)
though, even if you write out the constructor type with explicit
constraints and forall's.
E.g. by using a -XTypeApp
On Sat, Mar 20, 2021 at 08:13:18AM -0400, Viktor Dukhovni wrote:
> As soon as I try add more complex contraints, I appear to need an
> explicit type signature for HNil, and then the code again compiles:
But aliasing the promoted constructors via pattern synonyms, and using
those instead, appears
On Sat, Mar 20, 2021 at 04:40:59AM -0500, Alexis King wrote:
> Today I was writing some code that uses a GADT to represent
> heterogeneous lists:
>
> data HList as where
> HNil :: HList '[]
> HCons :: a -> HList as -> HList (a ': as)
>
> This type is used to provide a generic
Hi all,
Today I was writing some code that uses a GADT to represent
heterogeneous lists:
data HList as where
HNil :: HList '[]
HCons :: a -> HList as -> HList (a ': as)
This type is used to provide a generic way to manipulate n-ary
functions. Naturally, I have some functions
16 matches
Mail list logo
