Type class for sanity

[Richard Eisenberg]

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/f27cb01e/attachment.html>