Re: [Haskell-cafe] Recursive constraints with type families

23 Jan 2022

      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

Re: [Haskell-cafe] Recursive constraints with type families

Li-yao Xia