[Haskell-cafe] Recursive constraints with type families

[Li-yao Xia]

Hi Dmitriy,


On 2022-01-22 5:55 AM, Dmitriy Matrosov wrote:
> 
> I see, thanks. But what i've tried to implement is type-level countdown:
> 
[...]
>>
>> import GHC.TypeLits
>> import Data.Proxy
>> import Data.Kind
>> import qualified Fcf as F
>>
>> type C :: Nat -> Constraint
>> type family C x where
>>     C 0 = KnownNat 0
>>     C x = (KnownNat x, C (x - 1))
>>
>> countDown :: forall (n :: Nat). C n => Proxy n -> String
>> countDown _ = let x = natVal (Proxy @n)
>>               in  if x > 0
>>                     then show x ++ " " ++ countDown (Proxy @(n - 1))
>>                     else "end"
> 
> This code does not compile


The condition (x > 0) does not propagate any information at the type 
level. Such a thing is a feature of dependently typed languages, which 
Haskell is not. The compiler does not know that n > 0 in the first 
branch, so the constraint (C n) remains stuck.


> 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:
> 
>      *Main> :k! C2 3
>      ^CInterrupted.
>      *Main>
[...]
> May be someone can explain me, why it hangs? I'll be very grateful.


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


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"


Where the comparison (n > 0) is done at the type level and reflected by 
a boolean singleton value, of type SBool:


data SBool (a :: Bool) where
   SFalse :: SBool 'False
   STrue :: SBool 'True


Of course, the compiler doesn't know whether n is positive, so this 
information must be provided as a constraint (or derived somehow):


-- Add IsBool constraint in C2, for every If condition
data C2 :: Nat -> F.Exp Constraint
type instance F.Eval (C2 x) =
   (KnownNat x,
      IsBool (F.Eval (x F.> 0)),
      F.Eval (F.If (F.Eval (x F.> 0))
        (C2 (x - 1))
        (F.Pure (() :: Constraint))))


The IsBool class turns a known type-level boolean into a boolean 
singleton value indexed by that same boolean:


class IsBool b where
   getBool :: SBool b

instance IsBool 'True where
   getBool = STrue

instance IsBool 'False where
   getBool = SFalse


Full gist: https://gist.github.com/Lysxia/cf47807bbbcbb572896b350d66162a25

Regards,
Li-yao