[Haskell-cafe] Recursive constraints with type families
Dmitriy Matrosov
sgf.dma at gmail.com
Sat Jan 22 10:55:06 UTC 2022
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 <sgf.dma at gmail.com <mailto:sgf.dma at 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.
>
More information about the Haskell-Cafe
mailing list