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

On 1/21/22 8:30 PM, Georgi Lyubenov wrote:> Hi!

In order for you to reach any of the cases in C, the type family must be able to see if x is 0 or not. However, you're passing it an arbitrary n, so it has no way of knowing which case it should pick.

GHC doesn't do any reasoning of the sort "well this constraint is available in all the cases of the type family, so I'll just add it".

The solution here would be to separate your KnownNat constraint from whatever you want to calculate in your recursive type family:

type C1 n = (KnownNat n, C n) type family C n ...

countDown :: forall (n :: Nat). C1 n => Proxy n -> String countDown = ...

Hi, Georgi. 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> and using this as a constraint in 'countDown' results in: Prelude> :r [1 of 1] Compiling Main ( constraint-type-family-followup.lhs, interpreted ) constraint-type-family-followup.lhs:42:16: error: • Reduction stack overflow; size = 201 Though, adding the base case (and essentially making 'F.If' useless, but anyway)

type C2' :: Nat -> Constraint type family C2' x where C2' 0 = KnownNat 0 C2' x = F.If (F.Eval (x F.> 0)) (KnownNat x, C2' (x - 1)) (KnownNat 0)

fixes type calculation: *Main> :k! C2' 3 C2' 3 :: Constraint = (KnownNat 3, (KnownNat 2, (KnownNat 1, KnownNat 0))) but 'countDown' function does not compile with the same error as was with 'C'. May be someone can explain me, why it hangs? I'll be very grateful. And the other question, is how then should i implement such type-level count down function? Thanks.

Cheers,

Georgi

On Fri, Jan 21, 2022 at 7:00 PM Dmitriy Matrosov mailto:sgf.dma@gmail.com> wrote:

Hi.

I've stumbled upon a simple problem with recursive type family:

> {-# LANGUAGE RankNTypes #-} > {-# LANGUAGE KindSignatures #-} > {-# LANGUAGE TypeApplications #-} > {-# LANGUAGE TypeOperators #-} > {-# LANGUAGE PolyKinds #-} > {-# LANGUAGE TypeFamilies #-} > {-# LANGUAGE StandaloneKindSignatures #-} > {-# LANGUAGE ScopedTypeVariables #-} > {-# LANGUAGE UndecidableInstances #-} > > import GHC.TypeLits > import Data.Proxy > import Data.Kind > > type C :: Nat -> Constraint > type family C x where >     C 0 = KnownNat 0 >     --C x = (KnownNat x, C (x - 1)) >     C x = (KnownNat x, C 0) >     --C x = KnownNat x > > --type C2 x = (KnownNat x, C2 1) > > showNat :: forall (n :: Nat). C n => Proxy n -> String > showNat _ = show $ natVal (Proxy @n)

and the error is

     Prelude> :r      [1 of 1] Compiling Main             ( constraint-type-family.lhs, interpreted )

     constraint-type-family.lhs:31:22: error:          • Could not deduce (KnownNat n) arising from a use of ‘natVal’            from the context: C n              bound by the type signature for:                         showNat :: forall (n :: Nat). C n => Proxy n -> String              at constraint-type-family.lhs:30:3-56            Possible fix:              add (KnownNat n) to the context of                the type signature for:                  showNat :: forall (n :: Nat). C n => Proxy n -> String          • In the second argument of ‘($)’, namely ‘natVal (Proxy @n)’            In the expression: show $ natVal (Proxy @n)            In an equation for ‘showNat’: showNat _ = show $ natVal (Proxy @n)         |      31 | > showNat _ = show $ natVal (Proxy @n)         |                      ^^^^^^^^^^^^^^^^^

If i write just

      C x = KnownNat x

everything works fine. I guess, the reason is UndecidableInstances, but why and then, how can i build constraints recursively and make it work?

Thanks.

PS. Initially, this 'showNat' was something like

     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"

but it does not work.

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