Dear Cafe, let:
data True data False
class C a
(arbitrary instances for C may follow) Now, how to obtain an "Indicator Type" for C, i.e. a type IndC that is defined via a type family / fundep / ... , so that IndC a = True forall a which are instances of C IndC a = False for all other a. I've collected some failed approaches here[1]. My key problem is that if I define (in the 3rd try):
instance (C a) => IndC3 a True
, it does *not* mean "Define this instance for all a which are an instance of C", but "Define the instance IndC3 a True for all types a, but it's not gonna work if a is not an instance of C". Does anyone have another idea? Background: After having implemented type-level lists[2] and a quicksort on them[3], I'd like to have type-level sets. In their most simple implementation, sets are just (unsorted) lists like this:
data Nil data Cons a b class Elem x l (instances for Elem so that Elem x l iff x is an element of the list l)
Now I want:
type family Insert x s :: *
Insert x s = s forall (x, s) with (Elem x s) Insert x s = Cons x s for all other (x, s). Thanks a lot! Steffen [1] http://hpaste.org/fastcgi/hpaste.fcgi/view?id=25832#a25832 [2] Kiselyov, Peyton-Jones, Shan: "Fun with type functions" http://research.microsoft.com/en-us/um/people/simonpj/papers/assoc-types/fun... [3] I rewrote this algorithm using type families instead of fundeps: http://www.haskell.org/haskellwiki/Type_arithmetic#An_Advanced_Example_:_Typ...