[Haskell-cafe] Recursive constraints with type families
Li-yao Xia
lysxia at gmail.com
Wed Jan 26 15:14:35 UTC 2022
On 2022-01-26 9:51 AM, Dmitriy Matrosov wrote:
> So, the key of this trick is to make impossible to unfold type family
> without
> evaluating 'If' ?
>
Yes!
> I need something like
>
> type instance F.Eval (C2' 0) = (() :: Constraint)
> type instance F.Eval (C2' x) = (KnownNat x, F.Eval (C2' (x - 1)))
>
> which does not compile. Thus, i need If to be an argument for Eval (like in
> your code below), so ghc is forced to evaluate it to unfold type family
> further. Does this sound correct?
That sounds correct.
Another problem with closed type families here is that there is no
construct for "x is not 0" that would let you know to take the branch "C
x = (KnownNat x, C (x-1))". The general workaround used here is to turn
the comparison to a boolean and then reify that boolean. At that point,
you don't have to use `If`, you can also declare a new type family to
match on that boolean, but it gets tedious for the same reason we use
"if" at the term level rather than defining a new function for every
conditional.
> So, i can't use plain Bool with something like
>
> class IsBool b where
> getBool :: Proxy b -> Bool
>
> because in that case both True and False branches of case would have the
> same
> type and ghc can't figure out by looking at plain Bool whether type level
> condition (n F.> 0) was true or false, right?
>
Indeed.
> So, does ghc take condition from getBool application
> literally
> and then uses its result to evaluates If in type family?
That's right, GHC just takes the condition literally, it has no
understanding of the meaning of `>` and `+` to draw logical inferences
about them.
Nevertheless, you might be interested in ghc-typelits-natnormalize, a
plugin which equips GHC with a few such reasoning capabilities. Or
Liquid Haskell, for an even more powerful approach.
https://hackage.haskell.org/package/ghc-typelits-natnormalise
https://ucsd-progsys.github.io/liquidhaskell/
More information about the Haskell-Cafe
mailing list