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

23 Jan 2022

      On Saturday, January 22nd, 2022 at 11:55 AM, Dmitriy Matrosov  wrote:
[...]
...
I see, thanks. But what i've tried to implement is type-level countdown:
...
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE StandaloneKindSignatures #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE UndecidableInstances #-}
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 with
*Main> :r
     [1 of 1] Compiling Main             ( constraint-type-family-followup.lhs, interpreted )
constraint-type-family-followup.lhs:42:25: error:
         • Could not deduce (KnownNat n) arising from a use of ‘natVal’
           from the context: C n
             bound by the type signature for:
                        countDown :: forall (n :: Nat). C n => Proxy n -> String
             at constraint-type-family-followup.lhs:41:3-58
           Possible fix:
             add (KnownNat n) to the context of
               the type signature for:
                 countDown :: forall (n :: Nat). C n => Proxy n -> String
         • In the expression: natVal (Proxy @n)
           In an equation for ‘x’: x = natVal (Proxy @n)
           In the expression:
             let x = natVal (Proxy @n)
             in
               if x > 0 then
                   show x ++ " " ++ countDown (Proxy @(n - 1))
               else
                   "end"
        |
     42 | > countDown _ = let x = natVal (Proxy @n)
        |                         ^^^^^^^^^^^^^^^^^
constraint-type-family-followup.lhs:44:45: error:
         • Could not deduce: C (n - 1) arising from a use of ‘countDown’
           from the context: C n
             bound by the type signature for:
                        countDown :: forall (n :: Nat). C n => Proxy n -> String
             at constraint-type-family-followup.lhs:41:3-58
         • In the second argument of ‘(++)’, namely
             ‘countDown (Proxy @(n - 1))’
           In the second argument of ‘(++)’, namely
             ‘" " ++ countDown (Proxy @(n - 1))’
           In the expression: show x ++ " " ++ countDown (Proxy @(n - 1))
         • Relevant bindings include
             countDown :: Proxy n -> String
               (bound at constraint-type-family-followup.lhs:42:3)
        |
     44 | >                     then show x ++ " " ++ countDown (Proxy @(n - 1))
        |                                             ^^^^^^^^^^^^^^^^^^^^^^^^^^
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.
Unfortunately I have no idea. Fcf looks wild, I have no idea what's going on there.
...
And the other question, is how then should i implement such type-level count
down function?
Using type classes:
...
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE StandaloneKindSignatures #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE UndecidableInstances #-}
import GHC.TypeLits
import Data.Proxy
import Data.Kind
type CountDown :: Nat -> Constraint
class CountDown n where
    countDown :: Proxy n -> String
instance {-# OVERLAPPING #-} CountDown 0 where
    countDown _ = "end"
instance {-# OVERLAPPABLE #-} (CountDown (n - 1), KnownNat n) => CountDown n where
    countDown p = show (natVal p) ++ " " ++ countDown (Proxy @(n - 1))
Before I wrote this email I thought this would be possible using regular old type classes, but of course these instances are overlapping for the zero case. However, some pragmas make GHC do the right thing here.

Cheers,
Tom
...
Thanks.
[...]
...
_______________________________________________
Haskell-Cafe mailing list
To (un)subscribe, modify options or view archives go to:
http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
Only members subscribed via the mailman list are allowed to post.

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

Tom Smeding