# [Haskell-cafe] Recursive constraints with type families

Dmitriy Matrosov sgf.dma at gmail.com
Wed Jan 26 14:51:28 UTC 2022

```Hi Li-yao.

Thank you for detailed answer! It was really helpful, but i have a few more
questions.

On 1/24/22 12:05 AM, Li-yao Xia wrote:
> On 2022-01-22 5:55 AM, Dmitriy Matrosov wrote:
>>
>> If i try to get rid of cases in type family:
>>
>>> type C2 :: Nat -> Constraint
>>> type family C2 x where
>>>   C2 x = F.If (F.Eval (x F.> 0))
>>>           (KnownNat x, C2 (x - 1))
>>>           (KnownNat 0)
>>
>> ghc eats all memory and hangs during type family calculation:
>
> [...]
>
> The rule of thumb here is that if a type family can be unfolded, it will
> be, regardless of context. Since there is only one clause, (C2 x) can
> always be unfolded, and then C2 (x-1) will be unfolded (regardless of
> whether the "If" condition is true or false) and then (C2 ((x-1)-1)), etc.
>
> There is a trick with first-class-families to control evaluation with the
> Eval type family, by making the branches reduce to uninterpreted symbols,
> rather than type family applications.
>
> Two key components of this trick:
>
> - C2 must be a first-class type family (an "uninterpreted symbol")
> - Eval must be applied outside of If

So, the key of this trick is to make impossible to unfold type family without
evaluating 'If' ?

I mean, since

type C :: Nat -> Constraint
type family C x where
C 0 = KnownNat 0
C x = (KnownNat x, C (x - 1))

terminates, but

type instance F.Eval (C2' x) =
(KnownNat x,
--( F.If (F.Eval (x F.> 0))
( F.If 'False
(F.Eval (C2' (x - 1)))
(() :: Constraint)
)
)

hangs forever (even (F.If 'False) above makes no difference), i suppose, that
just having many type family instances (like Eval has) does not force ghc to
evaluate (x - 1) and If condition. 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?

>
> data C2 :: Nat -> F.Exp Constraint
> type instance F.Eval (C2 x) =
>    (KnownNat x,
>       F.Eval (F.If (F.Eval (x F.> 0))
>         (C2 (x - 1))
>         (F.Pure (() :: Constraint))))
>
> ghci:
>  > :k! F.Eval (C2 3)
> F.Eval (C2 3) :: Constraint
> = (KnownNat 3,
>     (KnownNat 2, (KnownNat 1, (KnownNat 0, () :: Constraint))))
>
>
>> And the other question, is how then should i implement such type-level count
>> down function?
>
> To make constraints sensitive to control-flow, you need at least GADTs. A
> general solution is provided by singletons, to simulate dependent types in
> singletons.
>
> One version of countdown looks like this:
>
>
> countdown :: forall n. F.Eval (C2 n) => Proxy n -> String
> countdown _ =
>    case getBool @(F.Eval (n F.> 0)) of
>      STrue -> show (natVal @n Proxy) ++ " " ++ countdown @(n-1) Proxy
>      SFalse -> "boom"

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?

Also, i've tried to make a slightly different conditions in type family and in
getBool application. E.g. if i use

getBool3 @(F.Eval ((n + 1) F.> 1))

then in type family only ((n + 1) F.> 1) or ((n + 1) F.> (0 + 1)) variants
will work, but with smth like (n F.> 0) ghc won't be able to resolve
constraints.  So, does ghc take condition from getBool application literally
and then uses its result to evaluates If in type family?

Thanks.
```