Type class for sanity

[Richard Eisenberg]

+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