Re: Type class for sanity

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" 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 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@haskell.org http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries