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
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...
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
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?
Is there a way to obtain the equivalent
Integer
from aNat
type?like
where
n
is of kindNat
@Bolt https://www.stackage.org/haddock/lts-14.15/base-4.12.0.0/GHC-TypeLits.html#v:natVal
awesome!!
I'm having this error
What I have
I've tried enabling RankNTypes and using forall but no success
"If I know which
n
it is, I can give youInteger
based on it :slight_smile: "already tried that :confused:
I've enabled ScopedTypeVariables
Still the same error
Do you have
forall
?Okay nailed it!
Needed to specify the kind
I guess
forall n.
will work as wellIt doesn't :frown:
With
PolyKinds
then? :sweat_smile:Have them enabled :confused:
Well actually it works now :sweat_smile:
I removed polykinds
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
ScopedTypeVariables
?Seeing what you're trying to do might be helpful, too.
Here the compiler complains about not being able to infer certain type constraints
I have
ScopedTypeVariables
enabled, and already tried to do something likeand use
ca
andra
but on the RHS the compiler infers other type names fora
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 samen
andm
it doesn't work unfortunately :frown:
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
https://stackoverflow.com/a/50788119 might have some thoughts
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
Maybe you need KnownNat constraints? I'm just throwing stuff at the wall, at this point
I have this:
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 ofa b c d
into scope so I can give the compiler the constraints it wants.. is there any way to do this?@Bolt most of the strategy here is having a rough idea of what's going wrong and throwing things at GHC until something works
which is to say people probably can't answer this for you without all of the code
my guess is you're running up against the noninjectivity of +
even though you know
m
andn
are each the sum of two things, you don't know which thingswhich is to say if i know
m + n = 15
there are infinite solutions for m and nthe solution is to store
Proxy m
andProxy n
inside the constructors forSplit
andJunc
for bonus points add
KnownNat
constraints in therethen you can pattern match on
Split
, pull out the relevant proxies, and rebuildJunc
with themwhich is a proof to GHC that these things have the same size you said they did
Interesting but that way the constructors will be a bit bloated :confused: I'll try it!
Thanks !!