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.

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

On 2022-01-26 9:51 AM, Dmitriy Matrosov wrote:

So, the key of this trick is to make impossible to unfold type family without evaluating 'If' ?

Yes!

I need something like

    type instance F.Eval (C2' 0) = (() :: Constraint)     type instance F.Eval (C2' x) = (KnownNat x, F.Eval (C2' (x - 1)))

which does not compile. Thus, i need If to be an argument for Eval (like in your code below), so ghc is forced to evaluate it to unfold type family further. Does this sound correct?

That sounds correct. Another problem with closed type families here is that there is no construct for "x is not 0" that would let you know to take the branch "C x = (KnownNat x, C (x-1))". The general workaround used here is to turn the comparison to a boolean and then reify that boolean. At that point, you don't have to use `If`, you can also declare a new type family to match on that boolean, but it gets tedious for the same reason we use "if" at the term level rather than defining a new function for every conditional.

So, i can't use plain Bool with something like

    class IsBool b where         getBool :: Proxy b -> Bool

because in that case both True and False branches of case would have the same type and ghc can't figure out by looking at plain Bool whether type level condition (n F.> 0) was true or false, right?

Indeed.

So, does ghc take condition from getBool application literally and then uses its result to evaluates If in type family?

That's right, GHC just takes the condition literally, it has no understanding of the meaning of `>` and `+` to draw logical inferences about them. Nevertheless, you might be interested in ghc-typelits-natnormalize, a plugin which equips GHC with a few such reasoning capabilities. Or Liquid Haskell, for an even more powerful approach. https://hackage.haskell.org/package/ghc-typelits-natnormalise https://ucsd-progsys.github.io/liquidhaskell/