Yes, if we can arrange that Ground a implies that Equals a [a] reduces to False, with
type family Equals a b where Equals a a = True Equals a b = False But getting that to work is admittedly a feature beyond what's proposed. On Jan 25, 2016, at 9:21 AM, Simon Peyton Jones <simo...@microsoft.com> wrote: > I’m a bit dubious about whether it’s worth the effort of making this an > extension that requires GHC support. Does the gain justify the (maybe-small > but eternal) pain > > Simon > > From: ghc-devs [mailto:ghc-devs-boun...@haskell.org] On Behalf Of Richard > Eisenberg > Sent: 25 January 2016 14:06 > To: David Feuer <david.fe...@gmail.com> > Cc: Haskell Libraries <librar...@haskell.org>; ghc-devs <ghc-devs@haskell.org> > Subject: Re: Type class for sanity > > Might be nice to have whnf too, while we're at it. Perhaps whnf is enough for > someone and going all the way to nf would be less efficient / impossible. > > Richard > > On Jan 25, 2016, at 8:44 AM, David Feuer <david.fe...@gmail.com> wrote: > > > I don't care about the name at all. Unstuck? Would we want to distinguish > between whnf (e.g., Proxy Any) and nf, or is only nf sufficiently useful? > > On Jan 25, 2016 7:34 AM, "Richard Eisenberg" <e...@cis.upenn.edu> wrote: > +1 > > This would be very easy to implement, too. > > But I suggest a different name. Ground? Terminating? NormalForm? Irreducible? > ValueType? I don't love any of these, but I love Sane less. > > On Jan 24, 2016, at 4:24 PM, David Feuer <david.fe...@gmail.com> wrote: > > > Since type families can be stuck, it's sometimes useful to restrict > > things to sane types. At present, the most convenient way I can see to > > do this in general is with Typeable: > > > > type family Foo x where > > Foo 'True = Int > > > > class Typeable (Foo x) => Bar x where > > blah :: proxy x -> Foo x > > > > This will prevent anyone from producing the bogus instance > > > > instance Bar 'False where > > blah _ = undefined > > > > Unfortunately, the Typeable constraint carries runtime overhead. One > > possible way around this, I think, is with a class that does just > > sanity checking and nothing more: > > > > class Sane (a :: k) > > instance Sane Int > > instance Sane Char > > instance Sane 'False > > instance Sane 'True > > instance Sane '[] > > instance Sane '(:) > > instance Sane (->) > > instance Sane 'Just > > instance Sane 'Nothing > > instance (Sane f, Sane x) => Sane (f x) > > > > To really do its job properly, Sane would need to have instances for > > all sane types and no more. An example of an insane instance of Sane > > would be > > > > instance Sane (a :: MyKind) > > > > which would include stuck types of kind MyKind. > > > > Would it be useful to add such an automatic-only class to GHC? > > > > David > > _______________________________________________ > > Libraries mailing list > > librar...@haskell.org > > http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries >
_______________________________________________ ghc-devs mailing list ghc-devs@haskell.org http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs
