#3447: Class restrictions on type instances
---------------------------------+------------------------------------------
Reporter: LysikovVV | Owner:
Type: feature request | Status: new
Priority: normal | Milestone: _|_
Component: Compiler | Version: 6.10.4
Severity: normal | Resolution:
Keywords: | Difficulty: Unknown
Testcase: | Os: Unknown/Multiple
Architecture: Unknown/Multiple |
---------------------------------+------------------------------------------
Comment (by conormcbride):
Replying to [comment:6 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 [http://personal.cis.strath.ac.uk/~conor/pub/she/ 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.
--
Ticket URL: <http://hackage.haskell.org/trac/ghc/ticket/3447#comment:7>
GHC <http://www.haskell.org/ghc/>
The Glasgow Haskell Compiler_______________________________________________
Glasgow-haskell-bugs mailing list
Glasgow-haskell-bugs@haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-bugs
