[Haskell-cafe] Type-level lazy bool operations
oleg at okmij.org
Thu Nov 26 09:18:40 UTC 2015
> Isn't the issue a bit more complex? The way I see it, the difference
> between the type level and the value level is that at the type level we
> want to do reasoning rather than just evaluation.
That is an excellent point! I wish the design of Haskell type-level
features has kept that in mind. For example, given the closed type
type family F1 a where
F1 Int = True
F1 a = False
type family F2 a where
F2 Int = Char
F2 a = Bool
wouldn't it be nice if (F1 a ~ True) were to simplify to (a ~ Int)?
Then the following term t1 would not have been ambiguous
data Proxy (a::Bool) = Proxy
foo :: Proxy (F1 a) -> a -> String
foo = undefined
t1 = foo (Proxy :: Proxy True) 1
And wouldn't it be nice if
(F1 a ~ False, F2 a ~ b) were to simplify to (b ~ Bool)?
Alas, such considerations were explicitly out of scope when type
families, open or closed, were designed. We wouldn't have had to wait
so long for injective type families; with the proper design, the need
for such feature would've been obvious from the beginning.
More information about the Haskell-Cafe