Suppose I have the following type:
type Control a = (a -> a) -> a -> a
I want exactly two values to inhabit this type when universally quantified:
break :: Control a
break = const id
continue :: Control a
continue = id
However, the astute amongst you would notice that Control a is the type of Church numerals, of which there are infinitely many. Is there any way to restrict this type so that the continuation can be applied at most once? Perhaps using dependent types?
Note that Control can appear in the context of a bigger function. For example:
mult :: Int -> Control Int
mult 0 = \k a -> k 0
mult b = \k a -> k (b * a)
As you can see \k a -> k (b * a) is neither break nor continue but is still a valid inhabitant of Control. However, it's not an inhabitant of Control a. It's an inhabitant of Control Int.
Thus, what I'm really asking is whether there's a way to check that a continuation is applied at most once at the type level.
We may recognize that const id is Church zero, and id is Church one, so we need Church naturals less than two - but if you want a two-element type, why not use Bool? Then interpret True as const id and False as id, or the other way. We can also say that Control a values are valid if they are in the image of the interpretation.
All types with two inhabitants are isomorphic, so if you restrict Control (which you could do with some dependent types), that would be just isomorphic to Bool. It makes more sense to define subsets of types when there isn't a compact standalone characterization of the subset.