See https://typesandkinds.wordpress.com/2015/09/09/what-are-type-families/ for some discussion. A type family application is stuck if it can't reduce further and has not reached a proper type. Given the aforementioned type family Foo, the application Foo 'False is stuck. It's a type of kind *, and it's uninhabited (but not as nicely uninhabited as Void--it offers no ex falso). This actually turns out to be useful for some things. GHC offers type family Any :: k where {} which is, at least, 1. A safe intermediate target for unsafeCoerce 2. An utterly unsatisfiable constraint (see the definition of Bottom in the GitHub master of the reflection package) But sometimes you want to know something's *not* a stuck type family. See the issue I filed earlier today at https://github.com/kwf/ComonadSheet/issues/6 for an example--the code tries to make a certain instance impossible to produce, but the possibility of stuckness defeats it as its currently written. On Jan 25, 2016 1:01 AM, "Jeffrey Brown" wrote:

"Stuck type" is proving difficult to Google. Do you recommend any references?

On Sun, Jan 24, 2016 at 1: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

-- Jeffrey Benjamin Brown

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

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

On Mon, Jan 25, 2016 at 7:34 AM, Richard Eisenberg wrote:

But I suggest a different name. Ground? Terminating? NormalForm? Irreducible? ValueType? I don't love any of these, but I love Sane less.

I'm also strongly opposed to using "sane". That name is ableist and quite offputting to many Haskellers I know (myself included). To say nothing of the fact that the name doesn't provide any useful understanding of what precisely it's supposed to be categorizing. -- Live well, ~wren