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 Haskell. For small tasks though, it's often easier to make your own 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.