Type class for sanity

[David Feuer]

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" <jeffbrown.the at gmail.com> wrote:

> "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 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
>>
>
>
>
> --
> Jeffrey Benjamin Brown
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/ghc-devs/attachments/20160125/5a3c0e49/attachment.html>