Class restrictions on type instances

[LysikovVV]

I'm using type families to implement bools and integers on type level.

There is a class BoolT with with two instances and type families representing usual boolean functions, e.g. NotT. By semantics of NotT, implication (BoolT a) => (BoolT (NotT a)) holds, but I cannot specify this to compiler, and using BoolT with NotT is painful.

So I think there must be syntactic construction to restrict type family instances to some class, something like

type family NotT a 
    with (BoolT a) => (BoolT (NotT a))

or

class BoolT a where
    type NotT a
        with BoolT (NotT a)

[LysikovVV]

Example

[simonpj]

The right thing seems to be to make BoolT (NotT a) a superclass, thus:

class BoolT (NotT a) => BoolT a where
   type NotT a

This is legal with -XFlexibleContexts. Perhaps you can see if that serves your purpose?

Simon

[LysikovVV]

Replying to simonpj:

This is legal with -XFlexibleContexts. Perhaps you can see if that serves your purpose?

    Cycle in class declarations (via superclasses):
      Bool.hs:(8,0)-(10,26): class (BoolT (NotT a)) => BoolT a where {
                                 type family NotT a; }

[simonpj]

Ah yes, sorry. I don't think I see a good way to achieve what you want, at least not without a new, ad-hoc extension.

Happily, though, what you want is to reject more programs. You can still write the programs you want.

Simon

[LysikovVV]

I have read your paper "Fun with type functions" and learned the concept of algebraic data kinds. This extension resolves the problem too. Is there plans to add it to GHC?

[simonpj]

Yes, definitely, I plan to add algebraic kinds. Timescale uncertain, though, I'm afraid.

Simon

[conormcbride]

Replying to simonpj:

Yes, definitely, I plan to add algebraic kinds. Timescale uncertain, though, I'm afraid.

I guess we should figure out how to proceed here.

This is an interesting example, exposing a number of issues. Firstly, and straightforwardly, how do we know Bool is closed under not: typechecking, if we had kind {Bool} inhabited by {True} and {False}. (Digression: whilst some sort of datakinds would be preferable to predicates here, predicate subkinding is still interesting and potentially of value.)

Secondly, what happens to choose if we have kind {Bool}? Note that choose is passed an element of some a for which BoolT a holds: the corresponding dictionary is a run-time witness to the ability to choose. What's needed here is not only that Bool is closed under not, but that run-time witnesses to Boolhood are closed under not.

The  she preprocessor lets us write

import ShePrelude -- includes {Bool}, {True}, {False}

type family    Not (b :: {Bool}) :: {Bool}
type instance  Not {True}   = {False}
type instance  Not {False}  = {True}

and we get the obvious nasty untyped translation, before typechecking. It would clearly be preferable to do the typechecking first, but if the semantics is the same, we've only bought security, not power. The question of how to manage run-time witnesses remains.

As it happens, she has an experimental treatment, based on a singleton translation. Roughly, if t is a type, then (:: t) is its singleton GADT. Moreover (subject to caveats) if tm :: ty, then {tm} :: (:: ty) {tm}, where the {tm} right of :: is the type-level translation and the {tm} left of :: is the singleton translation. For Bool, it's as if

data (:: Bool) :: {Bool} -> * where
  {True}   :: (:: Bool) {True}
  {False}  :: (:: Bool) {False}

More moreover, pi (x :: s). t abbreviates forall (x :: {s}) . (:: s) x -> t. So I can write

choose :: forall (t :: *). pi (b :: Bool). t -> t -> t
choose {True}   t f = t
choose {False}  t f = f

and even

boolCase :: forall (p :: {Bool} -> *). pi (b :: Bool).
            p {True} -> p {False} -> p b
boolCase {True}   t f = t
boolCase {False}  t f = f

However, to combine choose with Not, we need the relevant action on the run-time witnesses.

depNot :: pi (b :: Bool). (:: Bool) (Not b)
depNot {True}   = {False}
depNot {False}  = {True}

It's this depNot which delivers the extra information corresponding to the missing BoolT constraint requested above. We can then write

esoohc :: forall (t :: *). pi (b :: Bool). t -> t -> t
esoohc b = choose (depNot b)

It is clearly a nuisance to write type-level Not, together with value-level depNot, especially as yer actual not :: Bool -> Bool is a perfectly well-behaved proletarian.

What's my point? Just that algebraic kinds alone do not solve this problem: we need some principled system to manage the associated run-time witnesses. I'm used to getting this for nothing, of course -- dependent types identify the type-level data with their run-time witnesses -- so the thought of Joe manipulating classes and singleton GADTs explicitly in public makes me distinctly queasy. We don't have to solve this problem in order to add algebraic kinds, but we should be aware of it when we're making design choices.