Opened 6 years ago
Closed 3 months ago
#3447 closed feature request (fixed)
Class restrictions on type instances
Reported by: | LysikovVV | Owned by: | |
---|---|---|---|
Priority: | normal | Milestone: | ⊥ |
Component: | Compiler (Type checker) | Version: | 6.10.4 |
Keywords: | Cc: | Conor.McBride@… | |
Operating System: | Unknown/Multiple | Architecture: | Unknown/Multiple |
Type of failure: | None/Unknown | Test Case: | |
Blocked By: | Blocking: | ||
Related Tickets: | Differential Revisions: |
Description
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)
Attachments (1)
Change History (10)
Changed 6 years ago by LysikovVV
comment:1 Changed 6 years ago by igloo
- difficulty set to Unknown
- Milestone set to 6.14.1
comment:2 follow-up: ↓ 3 Changed 6 years ago by 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
comment:3 in reply to: ↑ 2 Changed 6 years ago by 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; }
comment:4 Changed 6 years ago by simonpj
- Milestone changed from 6.14.1 to _|_
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
comment:5 Changed 6 years ago by 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?
comment:6 follow-up: ↓ 7 Changed 6 years ago by simonpj
- Cc Conor.McBride@… added
Yes, definitely, I plan to add algebraic kinds. Timescale uncertain, though, I'm afraid.
Simon
comment:7 in reply to: ↑ 6 Changed 6 years ago by 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.
comment:8 Changed 3 months ago by thomie
- Component changed from Compiler to Compiler (Type checker)
- Type of failure set to None/Unknown
comment:9 Changed 3 months ago by goldfire
- Resolution set to fixed
- Status changed from new to closed
Example