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.
"Stuck type" is proving difficult to Google. Do you recommend any references?On Sun, Jan 24, 2016 at 1:24 PM, David Feuer <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.org
http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries
--Jeffrey Benjamin Brown