Re: Records in Haskell

Ryan Newton rrnewton at gmail.com writes: I admit I'm a big fan of polymorphic extension. But I don't love it enough for it to impede progress! Regarding extension: In trying to read through all this material I don't see a lot of love for lacks constraints a la TRex. Cheers,

Re: [Haskell-cafe] Some thoughts on Type-Directed Name

There is an effort underway to make Haskell's Records better. The discussion is ongoing on the ghc-users mail list, ... in the direction of making the most minimal changes possible to achieve some simple record name-spacing. Thanks, Greg Weber Thank you Greg, Yes I know, and I have been

Re: Records in Haskell

On Thu, Jan 26, 2012 at 8:02 PM, AntC anthony_clay...@clear.net.nz wrote: Ryan Newton rrnewton at gmail.com writes: I admit I'm a big fan of polymorphic extension. But I don't love it enough for it to impede progress! Records proposals for Haskell have repeatedly foundered

Re: simple extension to ghc's record disambiguation rules

Hi, I'd like to propose an extremely simple extension to ghc's record disambiguation rules, John, I've just posted a proposal on the 'Records in Haskell' wiki that I think will do the job for you. Declared Overloaded Record Fields (DORF). I'd appreciate feedback. my motivation is that I

Re: Records in Haskell

Actually, I looked at the SORF page again: http://hackage.haskell.org/trac/ghc/wiki/Records/OverloadedRecordFields There is now an 'Alternative Proposal' section that claims to solve polymorphic update. If anyone has comments on this please let us know! Yes, Greg the quasifunctor stuff has

Re: Records in Haskell

Whoa! suddenly a deluge over the DORF proposal. I don't have time to reply fully now, but I must say: Barney you have got it all wrong. No, DORF does not attach one class to each label. There is only one class 'Has', with methods get and set. Each record decl generates an instance for the

Re: Records in Haskell

Wren/all Please remember SPJ's request on the Records wiki to stick to the namespace issue. We're trying to make something better that H98's name clash. We are not trying to build some ideal polymorphic record system. To take the field labelled name: in H98 you have to declare each record in a

[ghc-devs]: Explicit inequality evidence

[transferring to -users, because there's a much wider discussion] > > On Dec 13, 2016, at 15:04, Richard Eisenberg wrote: > > I've thought about inequality on and off for years now, The subject has appeared (in various guises) on Haskell forums since well before 2002 [1] -- which went into the

Re: [ghc-devs]: Explicit inequality evidence

> On Dec 13, 2016, at 1:02 AM, David Feuer wrote: > >> On Tue, Dec 13, 2016 at 12:49 AM, Oleg Grenrus wrote: >> >> I assume that in your rules, variables are not type families, otherwise >> >> x /~ y => f x /~ f y doesn't hold if `f` isn't injective. (e.g. type family F x where F x = ()) >>

Re: DeriveFoldable treatment of tuples is surprising

> On Wed Mar 22 13:54:05 UTC 2017, Twan van Laarhoven wrote: >> On 2017-03-21 21:34, David Feuer wrote: >> This seems much too weird: >> >> *> :set -XDeriveFoldable >> *> data Foo a = Foo ((a,a),a) deriving Foldable >> *> length ((1,1),1) >> 1 >> *> length $ Foo ((1,1),1) >> 3 Hmm. *> length $

Why isn't this Overlapping?

--ghc 7.10 or 8.0.1 {-# LANGUAGE DataKinds, KindSignatures, GADTs, MultiParamTypeClasses, FunctionalDependencies, FlexibleInstances, UndecidableInstances, NoOverlappingInstances #-} class TypeEq a a' (b :: Bool) | a a' -> b instance (b ~

Re: Why isn't this Overlapping?

nce {-# OVERLAPPABLE #-} (b ~ Char) => C Int b where .. Then `foo (5 :: Int) undefined` ==> "Bool called" So GHC both uses the FunDep to improve the type, and uses the improvement to select an instance; and yet seems blind to FunDep inconsistencies in the instance dec

RE: Why isn't this Overlapping?

ing the first instance and `TypeEq a a False` >> using the second one. Unfortunately, the check that we are using >> to validate FDs when `UndecidableInstances` is on, >> is not quite correct (relevant tickets are #9210 and #10675 >> where there are similar examples)

Re: Trouble with injective type families

> On Wed Jul 5 14:16:10 UTC 2017, Richard Eisenberg wrote: > I'd like to add that the reason we never extended System FC > with support for injectivity is that the proof of soundness > of doing so has remained elusive. Thank you Richard, Simon. IIRC the original FDs through CHRs paper did think

Re: Superclass Equality constraints cp FunDeps

own that a superclass constraint with FunDeps on the superclass induces FunDeps on the sub-class without explicitly needing to declare so? (I'm not complaining, more surprised/impressed.) AntC > > On Apr 27, 2017, at 8:14 PM, Anthony Clayden > > <anthony_clay...@clear.net.nz>

Superclass Equality constraints cp FunDeps

The docos say [User Guide 10.14.1. on Equality Constraints] > Equality constraints can also appear in class and instance contexts. > The former enable a simple translation of programs using > functional dependencies into programs using family synonyms instead.

Re: Superclass Equality constraints cp FunDeps

> On at Apr 29 05:55:14 UTC 2017, Anthony Clayden wrote: > ... > So should I reasonably have known that > a superclass constraint > with FunDeps on the superclass > induces FunDeps on the sub-class > without explicitly needing to declare so? > > (I'm not complainin

Proposal: Instance apartness guards

After years of pondering this idea (in various forms), and several rounds of discussion on several forums, I've written it up. "This proposal tackles the thorny topic of Overlapping instances, for both type classes and Type Families/Associated types, by annotating instance heads with

Re: Superclass Equality constraints cp FunDeps

Now that I've got the bit between my teeth ... Superclass constraints are not subject to the Paterson conditions. IOW I can write superclass constraints that are not permitted as instance constraints. (Superclass constraints are required to be non-cyclic, which ensures they're terminating.) Is

Re: Superclass Equality constraints cp FunDeps

> On Sun Apr 30 19:35:17 UTC 2017 Brandon Allbery wrote: >> On Sun, Apr 30, 2017 at 3:31 PM, Richard Eisenberg wrote: >>> >>> On Apr 30, 2017, at 6:37 AM, Anthony Clayden wrote: >>> Is that behaviour officially documented somewhere? >> >> Not th

Re: Superclass Equality constraints cp FunDeps

inked my ticket to that one. AntC > > > On Apr 30, 2017, at 3:35 PM, Brandon Allbery wrote: >>> On Sun, Apr 30, 2017 at 3:31 PM, Richard Eisenberg wrote: >>>> On Apr 30, 2017, at 6:37 AM, Anthony Clayden wrote: >>>> Is that behaviour officially documen

Re: [was ghc-devs] Reasoning backwards with type families

. > On Nov 20, 2017 3:44 AM, "Anthony Clayden" <anthony_clay...@clear.net.nz> > wrote: > > > On Thu Nov 16 01:31:55 UTC 2017, David Feuer wrote: > > ... > > > > > For (&&), the obvious things you'd want are ... > > >

Re: [was ghc-devs] Reasoning backwards with type families

standing didn't represent genuine use cases? Is anybody out there using Injective Type Families currently? What for? AntC > On Mon, Nov 20, 2017 at 3:44 AM Anthony Clayden < > anthony_clay...@clear.net.nz> wrote: > >> > On Thu Nov 16 01:31:55 UTC 2017, David Feuer wro

Re: [was ghc-devs] Reasoning backwards with type families

ints and who-knows-what.) None of it is sound or complete or rugged, in particular you can't risk orphan instances -- unless plug3: https://github.com/ghc-proposals/ghc-proposals/pull/56#issuecomment-351289722 AntC > On Thu, Dec 14, 2017 at 11:29 AM, Anthony Clayden < > anthony_clay..

Re: [was ghc-devs] Reasoning backwards with type families

On Thu, 14 Dec 2017 at 4:13 PM, Clinton Mead wrote: > > I've panicked GHC enough whilst developing Freelude so whilst I'm not sure > exactly what you're saying I'd be hestiant about exploiting anything bogus > (8.2 btw seems far more stable than 8.0 btw). > ;-) Fair

Re: [was ghc-devs] Reasoning backwards with type families

> On Thu Nov 16 01:31:55 UTC 2017, David Feuer wrote: (Moving to ghc-users, there's nothing particularly dev-y.) > Sometimes it woulld be useful to be able to reason backwards > about type families. Hi David, this is a well-known issue/bit of a sore. Discussed much in the debate between type

Re: Proposal: Instance apartness guards

Surprisinlgy little comment on this proposal. Perhaps it landed when yous were busy elsewhere. I'd like to push it to the committee soon; this is an invitation for more feedback. Richard E wrote a nice brief summary https://github.com/ghc-proposals/ghc-proposals/pull/56#issuecomment-311421457

Scoped Type Variables discussion forum [was: open up the issues tracker on ghc-proposals]

This thread is a discussion about discussions, not the discussion itself ;-) I'm cc'ing to the cafe; but I'd prefer replies to come to glasgow-haskell-users. >> I can volunteer to at least scrape together all the objections to ScopedTypeVariables as currently. It's not yet a proposal, so not on

Re: Open up the issues tracker on ghc-proposals

> On Th, 3 May 2018 at 13:53 UTC, Joachim Breitner wrote: > I am worried about the signal-to-noise ratio for those poor committee > members who have not given up on following the GitHub notifications for > the ghc-proposals repository > > Almost by definition, Issue-tracker traffic should

Re: Scoped Type Variables discussion forum [was: open up the issues tracker on ghc-proposals]

On Wed, 9 May 2018 03:01 UTC, cheater00 wrote: > I couldn't live without ScopedTypeVariables. For me it's an essential tool when I want to figure out Yes absolutely. To be clear: nobody's talking about removing it. The question is, could we get the same functionality without being so confusing

Re: Scoped Type Variables discussion forum [was: open up the issues tracker on ghc-proposals]

ignature with data constructor looks the same whether or not the constructor is existentially-quantified. What's worse a constructor might have a mix of existential and universal variables. AntC > On Sat, May 19, 2018 at 2:56 PM, Brandon Allbery <allber...@gmail.com> > wrote: > &

Re: Open up the issues tracker on ghc-proposals

> On May 1, 2018, at 2:24 PM, David Feuer wrote: > > Sometimes, a language extension idea could benefit from some community discussion before it's ready for a formal proposal. Can I point out it's not only ghc developers who make proposals. I'd rather you post this idea more widely. As a

Re: Open up the issues tracker on ghc-proposals

doesn't raise a response. What if Github issues tracker just becomes another backwater where ideas go to get ignored? AntC > > | -Original Message- > | From: Glasgow-haskell-users | boun...@haskell.org> On Behalf Of Anthony Clayden > | Sent: 02 May 2018 02:34 >

Re: Open up the issues tracker on ghc-proposals

On Th, 3 May 2018 at 13:53 UTC, Joachim Breitner wrote: > I am worried about the signal-to-noise ratio for those poor committee members ... Thanks Joachim, Yes that's exactly the worry. So please tell the rest of us how to best use your collective time. First help yourselves/get your own shit

Quantified Constraints and Injectivity

I’m looking at the flurry of activity around Quantified Constraints [1, 2, 3], suggestion of uses for implication logic [4], and comments in the hs2017 paper “raise the expressive power of type classes … to first-order logic. … more expressive modelling …”[Abstract]. Consider modelling the logic

Re: Equality constraints (~): type-theory behind them

On Mon, 10 Dec 2018 at 6:12 PM, Anthony Clayden < anthony_clay...@clear.net.nz> wrote: > On Mon, 10 Dec 2018 at 9:36 PM, Tom Schrijvers wrote: > >> Maybe our Haskell'17 paper about Elaboration on Functional Dependencies >> sheds some more light on your problem: >> &g

Re: Equality constraints (~): type-theory behind them

On Sat, 22 Dec 2018 at 8:01 PM, Oliver Charles wrote: On Sat, Dec 22, 2018 at 11:08 AM Anthony Clayden > wrote: > > > So the paper's main motivation is wrt Trac #9670. > > Are you sure you mean #9670? > Oops. Thanks for the catch Oliver. That should be #9627. (One

Re: Equality constraints (~): type-theory behind them

On Sat, 22 Dec 2018 at 7:08 PM, Anthony Clayden < anthony_clay...@clear.net.nz> wrote: > > On Mon, 10 Dec 2018 at 6:12 PM, Anthony Clayden < > anthony_clay...@clear.net.nz> wrote: > >> On Mon, 10 Dec 2018 at 9:36 PM, Tom Schrijvers wrote: >> >>>

Re: Equality constraints (~): type-theory behind them

riables, this > cannot be solved by unification. However, the local assumption (given > constraint) `a ~ b` can be used to solve this wanted. > > This is rather like automatically inferring where `typeCast` needs to be > placed (indeed, at the Core level there is a construct for casting b

Equality constraints (~): type-theory behind them

The (~) constraint syntax is enabled by either `GADTs` or `TypeFamilies` language extension. GADTs/Assoc Data Types/Assoc Type Synonyms/Type Families arrived in a series of papers 2005 to 2008, and IIRC the development wasn't finished in full in GHC until after that. (Superclass constraints took

Re: Equality constraints (~): type-theory behind them

ec 8, 2018 at 6:42 AM Anthony Clayden < > anthony_clay...@clear.net.nz> wrote: > >> On Fri, 7 Dec 2018 at 10:57 PM, Adam Gundry wrote: >> >>> >>> Regarding inference, the place that comes to mind is Vytiniotis et al. >>> OutsideIn(X): >>> >

Re: Equality constraints (~): type-theory behind them

ld be fixed and > *still* translate into FC. If anyone would like to work on that, I’d be > happy to help explain how the current machinery works. > > > > Simon > > > > *From:* Glasgow-haskell-users *On > Behalf Of *Anthony Clayden > *Sent:* 25 March 2019 11:50 &

Re: props for Hugs over System FC

On Mon, Mar 25, 2019 at 6:24 PM Anthony Clayden < anthony_clay...@clear.net.nz> wrote: >... > Errk. pasted the wrong example. The code that works is class F a b | a -> b instance F Int Bool class D a where { op :: (F a b) => a -> b } instance (TypeC

props for Hugs over System FC

heh heh. I've got to record this for posterity. I've never known an example before. Some code that compiles in Hugs and works fine; but GHC (8.6.4) can't typecheck so rejects. It's an example in the 2011 'System F with Type Equality Coercions', section 2.3 discussing FunDeps; and used to justify

Re: Equality constraints (~): type-theory behind them

> On Mon, Dec 10, 2018 at 8:36:42 AM Tom Schrijvers wrote: > Maybe our Haskell'17 paper about Elaboration on Functional Dependencies sheds some more light on your problem: Thanks Tom, I've also been working through the 2011 expanded version of 'System F with Type Equality Coercions' that Adam

Re: [Haskell-cafe] Final steps in GHC's Trac-to-GitLab migration

>On March 6, 2019 11:21:34 UTC, Ben Gamari wrote: >>On March 6, 2019 6:11:49 AM EST, Ara Adkins wrote:>>*One question: what is >>happening with the trac tickets mailing list? I *>>*imagine it’ll be going away, but for those of us that use it to keep *>>*track of things is there a recommended

Constraints on type synonyms

Consider >pattern PPoint :: Floating a => a -> a -> (a, a) -- => () >pattern PPoint x y = (x, y) >originP = PPoint 0 0 >scaleP w (PPoint x y) = PPoint (w*x) (w*y) Inferred `scaleP :: Floating a => a -> (a, a) -> (a, a)` -- so more restrictive than the `Num a` that would be

How to user-define a type equality constraint?

Type equality `(~)` is a fine constraint. It's mildly annoying I need either `-XGADTs` or `-XTypeFamilies` to use it -- because I don't otherwise need those extensions. OTOH it's not H2010 so it needs to be switched on somehow. I see the Committee is discussing what to do. It's to be enabled by

Re: How to user-define a type equality constraint?

> But why does this matter? Because I want the semantics of that equality constraint, without switching on any of these, which I don't otherwise use: GADTs TypeFamilies TypeOperators And if that means I can't use infix `~` in my constraints, I'll put up with that. (I'd user-define a

Pattern synonym 'Required' constraints === Datatype Contexts(?)

I must be slow on the uptake. I've just grokked this equivalence -- or is it? Consider >data Eq a => Set a = NilSet | ConsSet a (Set a) -- from the Language report > >-- ConsSet :: forall a. Eq a => a -> Set a => Set a -- inferred/per report > >-- equiv with Pattern syn

Re: Pattern synonym 'Required' constraints === Datatype Contexts(?)

Thank you Richard, Lennart, *Gergő* >* pattern Positive :: (Ord a, Num a) => a* >* pattern Positive <- ((>0) -> True)* *Heh heh, there's another surprise/undocumented 'feature'.* *It's not necessary to give a signature for pattern `Positive`, GHC will infer that from the decl.* *I was

Re: InstanceSigs -- rationale for the "must be more polymorphic than"

> If you would like to offer a patch for the user manual to explain this better, that would be great. Thank you Simon for the invitation. On further investigation https://gitlab.haskell.org/ghc/ghc/-/issues/20357, what I'd like the user manual to say is: "InstanceSigs is a mis-feature. Don't

Was: [Haskell-cafe] Haskell reference documentation, laws first or laws last?

(Moving this discussion to glasgow-users. It's just not appropriate on the cafe.) > I am no longer a novice, and yet would still have a hard time making any use of the laws as written in constructing instances. Instead, I'd ignore the laws and write a natural intuitive instance, and it would

InstanceSigs -- rationale for the "must be more polymorphic than"

I can't help but feel InstanceSigs are either superfluous or upside-down. It's this bit in the User Guide: > The type signature in the instance declaration must be > more polymorphic than (or the same as) the one in the class declaration, > instantiated with the instance type. Usually if you

Re: InstanceSigs -- rationale for the "must be more polymorphic than"

mgu of the InstanceSig given with the substitution from the instance head & constraints. > > > *From:* Glasgow-haskell-users *On > Behalf Of *David Feuer > *Sent:* 08 August 2021 09:37 > *To:* Anthony Clayden > *Cc:* GHC users > *Subject:* Re: InstanceSigs -- rati

Re: Pattern synonym constraints :: Ord a => () => ...

On Wed, 6 Oct 2021 at 21:24, Simon Peyton Jones wrote: > > > I suggest the User Guide needs an example where a constraint needed for > matching (presumably via a View pattern) is not amongst the > constraints carried inside the data constructor, nor amongst those needed > for building. Then the

Pattern synonym constraints :: Ord a => () => ...

Thank you to Richard for the Tweag tutorials on Pattern Synonyms. That third one on Matchers was heavy going. I didn't find an answer (or did I miss it?) to something that's bugging me: >pattern SmartConstr :: Ord a => () => ... Seems to mean: * Required constraint is Ord a -- fine, for

Re: Pattern synonym constraints :: Ord a => () => ...

Richard Eisenberg wrote: > > > On Oct 3, 2021, at 5:38 AM, Anthony Clayden > wrote: > > >pattern SmartConstr :: Ord a => () => ... > > Seems to mean: > > * Required constraint is Ord a -- fine, for building > > > Yes.

Re: Pattern synonym constraints :: Ord a => () => ...

or synonyms (giving them separate > namespaces) would be a much simpler design. > > On Tue, Oct 5, 2021, 12:33 PM Richard Eisenberg > wrote: > >> >> >> On Oct 3, 2021, at 5:38 AM, Anthony Clayden >> wrote: >> >> >pattern SmartConstr :: Ord a =>

Re: Pattern synonym constraints :: Ord a => () => ...

ume the Provided constraints -- in > > other words, those constraints are "provided" to you by the pattern > > synonym. > > > > It is true that the builder could have entirely unrelated constraints > > to either (as in the proposal). The current implem

Typing of Pattern Synonyms: Required vs Provided constraints

There was an interesting exchange between the authors of Haskell compilers back in 1999 (i.e. when there were multiple compilers) http://web.archive.org/web/20151001142647/http://code.haskell.org/~dons/haskell-1990-2000/msg04061.html I was trying to simulate SPJ's point of view, using

Re: Typing of Pattern Synonyms: Required vs Provided constraints

On Fri, 7 Jan 2022 at 09:08, Richard Eisenberg wrote: > > > On Jan 5, 2022, at 9:19 PM, Anthony Clayden > wrote: > > So Pattern syns seem to be giving exactly the 'stupid theta' behaviour. > > > In your example, yes: the Required context is "stupid&

Fwd: Typing of Pattern Synonyms: Required vs Provided constraints

Thanks Gergö, I do find Richard's tendency to use ViewPattern examples distracts me from understanding the point. That arrow-to-nowhere or arrow-to-the-wrong-value syntax is nausea-inducing. Your "instructive" example is really nothing to do with PatSyns, just ordinary Haskell numeric patterns:

Re: Typing of Pattern Synonyms: Required vs Provided constraints [was cafe DatatypeContexts / alternative]

nd-in for the invariant: no duplicates; elements in ascending sequence; BST balanced. So the Monoid instance still couldn't expose the underlying data constructors. Forcing to use `foldMap` at least puts it in the programmer's face that trying to use `fmap` is a type error standing in for law-breakin

Re: [ANNOUNCE] GHC 9.4.1 is now available

Thanks Ben, there's a couple of broken links on the Downloads page, going via the haskell.org/ghc 'GHC 9.4.1 Released!' link, rather than the link below in your message: * Release Notes * Documentation The urls seem to be using a different directory structure, ==> 404. (Also the link in your

data families/newtype instances allow `DatatypeContext`s ?

https://discourse.haskell.org/t/choosing-data-representation-based-on-type/5970/4?u=antc2 A `DatatypeContext` on a `newtype instance` gets the usual warning it's deprecated. But the decl is accepted -- at GHC 8.10. (It doesn't achieve what the O.P. was asking for -- but then I wouldn't expect it

Pattern Synonym decls only at top level

" Pattern synonym declarations can only occur in the top level of a module. In particular, they are not allowed as local definitions. " says the User Guide. And the 2016 paper says likewise. But there's no explanation why. PattSyns are not necessarily declared in the same module as the