Type class for sanity

[Simon Peyton Jones]

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<mailto: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<mailto: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<mailto: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<mailto:Libraries at haskell.org>
> http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries<https://na01.safelinks.protection.outlook.com/?url=http%3a%2f%2fmail.haskell.org%2fcgi-bin%2fmailman%2flistinfo%2flibraries&data=01%7c01%7csimonpj%40064d.mgd.microsoft.com%7cdd2a26ab307a45b5f56808d32590ab5b%7c72f988bf86f141af91ab2d7cd011db47%7c1&sdata=cEc6WoMyDqd3ulJ6UenlCm%2bpeYdQ4z2FMSNcXkg8Qpc%3d>

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