[Haskell-cafe] Recursive constraints with type families

[Tom Smeding]

On Saturday, January 22nd, 2022 at 11:55 AM, Dmitriy Matrosov <sgf.dma at gmail.com> 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.