Type class for sanity

[Richard Eisenberg]

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 <simonpj at 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-bounces at haskell.org] On Behalf Of Richard Eisenberg
> Sent: 25 January 2016 14:06
> To: David Feuer <david.feuer at gmail.com>
> Cc: Haskell Libraries <libraries at haskell.org>; ghc-devs <ghc-devs at 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.feuer at 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" <eir at 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.feuer at 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
> > Libraries at haskell.org
> > http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries
> 

-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/ghc-devs/attachments/20160125/f7f74ffa/attachment-0001.html>