Obtaining Integer from Nat - Haskell

Welcome to the Functional Programming Zulip Chat Archive. You can join the chat here.

Bolt

Is there a way to obtain the equivalent Integer from a Nat type?

Bolt

like

f :: T n
f = n

where n is of kind Nat

Bolt

I'm having this error

Could not deduce (KnownNat n0) arising from a use of natVal

What I have

data T (n :: Nat) = T n

f :: T n -> Integer
f _ = natVal (Proxy :: Proxy n)
Bolt

I've tried enabling RankNTypes and using forall but no success

TheMatten
f :: KnownNat n => T n -> Integer

"If I know which n it is, I can give you Integer based on it :slight_smile: "

Bolt

already tried that :confused:

Could not deduce (KnownNat n0) arising from a use of natVal
      from the context: KnownNat n
Bolt

I've enabled ScopedTypeVariables

Bolt

Still the same error

TheMatten

Do you have forall?

Bolt

Okay nailed it!

f :: forall (n :: Nat) . T n -> Integer
f _ = natVal (Proxy :: Proxy n)

Needed to specify the kind

TheMatten

I guess forall n. will work as well

Bolt

It doesn't :frown:

TheMatten

With PolyKinds then? :sweat_smile:

Bolt

Have them enabled :confused:

Bolt

Well actually it works now :sweat_smile:

Bolt

I removed polykinds

Bolt

Is it possible to get function argument types in scope and constraint them? Everytime I try to do that the compiler infers different variable types in the RHS

Jack Henahan

Seeing what you're trying to do might be helpful, too.

Bolt
abide :: Matrix e n m -> Matrix e n m
abide (One e) = One e
abide (Split (Junc a b) (Junc c d)) = Junc (Split a c) (Split b d)
abide (Junc (Split a c) (Split b d)) = Split (Junc a b) (Junc c d)

Here the compiler complains about not being able to infer certain type constraints

Could not deduce: n3 ~ n2
      from the context: (n ~ (m1 + n1), ValidDimensions m1 n1, NonZero m)
        bound by a pattern with constructor:
                   Junc :: forall (m :: Nat) (n :: Nat) (p :: Nat) e.
                           (ValidDimensions m n, NonZero p) =>
                           Matrix e m p -> Matrix e n p -> Matrix e (m + n) p,
                 in an equation for abide
        at /home/bolt/Desktop/Bolt/UMinho/5ºAno/Tese/Playground/LAoP/src/Matrix.hs:329:8-35
      or from: (m ~ (m2 + n2), ValidDimensions m2 n2, NonZero m1)
        bound by a pattern with constructor:
                   Split :: forall (m :: Nat) (n :: Nat) (p :: Nat) e.
                            (ValidDimensions m n, NonZero p) =>
                            Matrix e p m -> Matrix e p n -> Matrix e p (m + n),
                 in an equation for abide
        at /home/bolt/Desktop/Bolt/UMinho/5ºAno/Tese/Playground/LAoP/src/Matrix.hs:329:14-22
      or from: (m ~ (m3 + n3), ValidDimensions m3 n3, NonZero n1)
        bound by a pattern with constructor:
                   Split :: forall (m :: Nat) (n :: Nat) (p :: Nat) e.
                            (ValidDimensions m n, NonZero p) =>
                            Matrix e p m -> Matrix e p n -> Matrix e p (m + n),
                 in an equation for abide
        at /home/bolt/Desktop/Bolt/UMinho/5ºAno/Tese/Playground/LAoP/src/Matrix.hs:329:26-34
      n3 is a rigid type variable bound by
        a pattern with constructor:
          Split :: forall (m :: Nat) (n :: Nat) (p :: Nat) e.
                   (ValidDimensions m n, NonZero p) =>
                   Matrix e p m -> Matrix e p n -> Matrix e p (m + n),
        in an equation for abide
        at /home/bolt/Desktop/Bolt/UMinho/5ºAno/Tese/Playground/LAoP/src/Matrix.hs:329:26-34
      n2 is a rigid type variable bound by
        a pattern with constructor:
          Split :: forall (m :: Nat) (n :: Nat) (p :: Nat) e.
                   (ValidDimensions m n, NonZero p) =>
                   Matrix e p m -> Matrix e p n -> Matrix e p (m + n),
        in an equation for abide
        at /home/bolt/Desktop/Bolt/UMinho/5ºAno/Tese/Playground/LAoP/src/Matrix.hs:329:14-22
      Expected type: Matrix e n1 n2
        Actual type: Matrix e n1 n3
     In the second argument of Junc, namely d
      In the second argument of Split, namely (Junc c d)
      In the expression: Split (Junc a b) (Junc c d)
     Relevant bindings include
        d :: Matrix e n1 n3
        c :: Matrix e m1 n2
Bolt

I have ScopedTypeVariables enabled, and already tried to do something like

abide (Split (Junc (a :: Matrix e ca ra) b) (Junc c d)) = Junc (Split a c) (Split b d)

and use ca and ra but on the RHS the compiler infers other type names for a

Jack Henahan

I think you'll need to do forall n m. Matrix e n m -> Matrix e n m to make it believe that they're the same n and m

Bolt

it doesn't work unfortunately :frown:

Jack Henahan

Oh, I see, there's Nat math going on. I've totally forgotten what the dumb thing you have to do is to make GHC okay with that

Jack Henahan

https://stackoverflow.com/a/50788119 might have some thoughts

I'm playing around with what tools haskell offers for dependently typed programming. I have promoted a GADT representing natural numbers to the kind level and made a type family for addition of nat...
Bolt

damn that's messed up :frown: I don't think I need to prove any property I just need to get the constraints right, and I can't because GHC doesn't let me tell him the names for the type variables

Jack Henahan

Maybe you need KnownNat constraints? I'm just throwing stuff at the wall, at this point

Bolt

I have this:

abide :: forall n m e . Matrix n m e -> Matrix n m e
abide (Junc (Split a c) (Split b d)) = Split (Junc a b) (Junc c d)

And GHC complains about not being able to infer the constraints on the types of a b c d... And I'm not able to bring the types of a b c d into scope so I can give the compiler the constraints it wants.. is there any way to do this?

Sandy Maguire

@Bolt most of the strategy here is having a rough idea of what's going wrong and throwing things at GHC until something works

Sandy Maguire

which is to say people probably can't answer this for you without all of the code

Sandy Maguire

my guess is you're running up against the noninjectivity of +

Sandy Maguire

even though you know m and n are each the sum of two things, you don't know which things

Sandy Maguire

which is to say if i know m + n = 15 there are infinite solutions for m and n

Sandy Maguire

the solution is to store Proxy m and Proxy n inside the constructors for Split and Junc

Sandy Maguire

for bonus points add KnownNat constraints in there

Sandy Maguire

then you can pattern match on Split, pull out the relevant proxies, and rebuild Junc with them

Sandy Maguire

which is a proof to GHC that these things have the same size you said they did

Bolt

Interesting but that way the constructors will be a bit bloated :confused: I'll try it!