Mixing
Recursion through Nat-kinds
.everyoneloves__top-leaderboard:empty,.everyoneloves__mid-leaderboard:empty,.everyoneloves__bot-mid-leaderboard:empty{ height:90px;width:728px;box-sizing:border-box;
}
This question is a sequel to the following question. Refer to it first:
Overlapping instances via Nat-kind
Now it's time to make the instance of Group Symmetric. After some savage math, I've come up to an instance that works in principle, but actually doesn't:
sIndex :: forall n. KnownNat n => Symmetric n -> Integer -> Integer
sIndex xs m = sIndex_ xs (m `mod` n)
where
n = toInteger (natVal (Proxy :: Proxy n))
sIndex_ :: Symmetric m -> Integer -> Integer
sIndex_ S1 _ = 0
sIndex_ (x :. _) 0 = cIndex x
sIndex_ (x :. xs) m = let
i = cIndex x + sIndex_ xs (m-1)
in if i < n then i else i - n
instance KnownNat n => Semigroup (Symmetric n) where
x <> y = go n where
n = toInteger (natVal (Proxy :: Proxy n))
go :: forall m. [(Integer,Integer)] -> Integer -> Symmetric m
go j m
| 0 == m = S1
| otherwise = let
i = sIndex y (sIndex x (n-m))
ix = foldr f i j
in cyclic ix :. go ((ix,m) :j) (m-1)
f (j,m) i = (i - j) `mod` m - 1
The go function inside the Semigroup instance should build the result by having recursion though Symmetric n, Symmetric (n-1), and so on until Symmetric 1. But GHC doesn't know how to do it and outputs the following error message:
Group_Symmetric.hs:89:24: error:
• Couldn't match type ‘m’ with ‘1’
‘m’ is a rigid type variable bound by
the type signature for:
go :: forall (m :: Nat).
[(Integer, Integer)] -> Integer -> Symmetric m
at Group_Symmetric.hs:87:9-69
Expected type: Symmetric m
Actual type: Symmetric 1
So what would the workaround be? Is it possible for go to be able to return any instantation of Symmetric m (m from 1 to n)?
haskell recursion math gadt data-kinds
asked Jan 3 at 4:50
Dannyu NDosDannyu NDos
1,015723
add a comment |
This question is a sequel to the following question. Refer to it first:
Overlapping instances via Nat-kind
Now it's time to make the instance of Group Symmetric. After some savage math, I've come up to an instance that works in principle, but actually doesn't:
sIndex :: forall n. KnownNat n => Symmetric n -> Integer -> Integer
sIndex xs m = sIndex_ xs (m `mod` n)
where
n = toInteger (natVal (Proxy :: Proxy n))
sIndex_ :: Symmetric m -> Integer -> Integer
sIndex_ S1 _ = 0
sIndex_ (x :. _) 0 = cIndex x
sIndex_ (x :. xs) m = let
i = cIndex x + sIndex_ xs (m-1)
in if i < n then i else i - n
instance KnownNat n => Semigroup (Symmetric n) where
x <> y = go n where
n = toInteger (natVal (Proxy :: Proxy n))
go :: forall m. [(Integer,Integer)] -> Integer -> Symmetric m
go j m
| 0 == m = S1
| otherwise = let
i = sIndex y (sIndex x (n-m))
ix = foldr f i j
in cyclic ix :. go ((ix,m) :j) (m-1)
f (j,m) i = (i - j) `mod` m - 1
The go function inside the Semigroup instance should build the result by having recursion though Symmetric n, Symmetric (n-1), and so on until Symmetric 1. But GHC doesn't know how to do it and outputs the following error message:
Group_Symmetric.hs:89:24: error:
• Couldn't match type ‘m’ with ‘1’
‘m’ is a rigid type variable bound by
the type signature for:
go :: forall (m :: Nat).
[(Integer, Integer)] -> Integer -> Symmetric m
at Group_Symmetric.hs:87:9-69
Expected type: Symmetric m
Actual type: Symmetric 1
So what would the workaround be? Is it possible for go to be able to return any instantation of Symmetric m (m from 1 to n)?
haskell recursion math gadt data-kinds
asked Jan 3 at 4:50
Dannyu NDosDannyu NDos
1,015723
add a comment |
This question is a sequel to the following question. Refer to it first:
Overlapping instances via Nat-kind
Now it's time to make the instance of Group Symmetric. After some savage math, I've come up to an instance that works in principle, but actually doesn't:
sIndex :: forall n. KnownNat n => Symmetric n -> Integer -> Integer
sIndex xs m = sIndex_ xs (m `mod` n)
where
n = toInteger (natVal (Proxy :: Proxy n))
sIndex_ :: Symmetric m -> Integer -> Integer
sIndex_ S1 _ = 0
sIndex_ (x :. _) 0 = cIndex x
sIndex_ (x :. xs) m = let
i = cIndex x + sIndex_ xs (m-1)
in if i < n then i else i - n
instance KnownNat n => Semigroup (Symmetric n) where
x <> y = go n where
n = toInteger (natVal (Proxy :: Proxy n))
go :: forall m. [(Integer,Integer)] -> Integer -> Symmetric m
go j m
| 0 == m = S1
| otherwise = let
i = sIndex y (sIndex x (n-m))
ix = foldr f i j
in cyclic ix :. go ((ix,m) :j) (m-1)
f (j,m) i = (i - j) `mod` m - 1
The go function inside the Semigroup instance should build the result by having recursion though Symmetric n, Symmetric (n-1), and so on until Symmetric 1. But GHC doesn't know how to do it and outputs the following error message:
Group_Symmetric.hs:89:24: error:
• Couldn't match type ‘m’ with ‘1’
‘m’ is a rigid type variable bound by
the type signature for:
go :: forall (m :: Nat).
[(Integer, Integer)] -> Integer -> Symmetric m
at Group_Symmetric.hs:87:9-69
Expected type: Symmetric m
Actual type: Symmetric 1
So what would the workaround be? Is it possible for go to be able to return any instantation of Symmetric m (m from 1 to n)?
haskell recursion math gadt data-kinds
asked Jan 3 at 4:50
Dannyu NDosDannyu NDos
1,015723
This question is a sequel to the following question. Refer to it first:
Overlapping instances via Nat-kind
Now it's time to make the instance of Group Symmetric. After some savage math, I've come up to an instance that works in principle, but actually doesn't:
sIndex :: forall n. KnownNat n => Symmetric n -> Integer -> Integer
sIndex xs m = sIndex_ xs (m `mod` n)
where
n = toInteger (natVal (Proxy :: Proxy n))
sIndex_ :: Symmetric m -> Integer -> Integer
sIndex_ S1 _ = 0
sIndex_ (x :. _) 0 = cIndex x
sIndex_ (x :. xs) m = let
i = cIndex x + sIndex_ xs (m-1)
in if i < n then i else i - n
instance KnownNat n => Semigroup (Symmetric n) where
x <> y = go n where
n = toInteger (natVal (Proxy :: Proxy n))
go :: forall m. [(Integer,Integer)] -> Integer -> Symmetric m
go j m
| 0 == m = S1
| otherwise = let
i = sIndex y (sIndex x (n-m))
ix = foldr f i j
in cyclic ix :. go ((ix,m) :j) (m-1)
f (j,m) i = (i - j) `mod` m - 1
The go function inside the Semigroup instance should build the result by having recursion though Symmetric n, Symmetric (n-1), and so on until Symmetric 1. But GHC doesn't know how to do it and outputs the following error message:
Group_Symmetric.hs:89:24: error:
• Couldn't match type ‘m’ with ‘1’
‘m’ is a rigid type variable bound by
the type signature for:
go :: forall (m :: Nat).
[(Integer, Integer)] -> Integer -> Symmetric m
at Group_Symmetric.hs:87:9-69
Expected type: Symmetric m
Actual type: Symmetric 1
So what would the workaround be? Is it possible for go to be able to return any instantation of Symmetric m (m from 1 to n)?
haskell recursion math gadt data-kinds
haskell recursion math gadt data-kinds
asked Jan 3 at 4:50
Dannyu NDosDannyu NDos
1,015723
asked Jan 3 at 4:50
Dannyu NDosDannyu NDos
1,015723
edited Jan 3 at 7:43
Dannyu NDos
asked Jan 3 at 4:50
Dannyu NDosDannyu NDos
1,015723
asked Jan 3 at 4:50
Dannyu NDosDannyu NDos
1,015723
asked Jan 3 at 4:50
Dannyu NDosDannyu NDos
1,015723
1,015723
add a comment |
add a comment |
1 Answer
1
active
oldest
votes
A slight change of go and f solved the problem:
instance KnownNat n => Semigroup (Symmetric n) where
x <> y = go x n where
n = toInteger (natVal (Proxy :: Proxy n))
go :: forall m. Symmetric m -> [(Integer,Integer)] -> Integer -> Symmetric m
go S1 _ _ = S1
go (_ :. xs) j m = let
i = sIndex x (sIndex y (n-m))
ix = foldr f i j
in Cyclic ix :. go xs ((ix,m) :j) (m-1)
f (j,m) i = let
ix = (i - j) `mod` m - 1
in if 0 <= ix then ix else ix + m
The key idea is to introduce a dummy parameter. Also note that Cyclic was used instead of cyclic.
Unfortunately, it turns out that I did some math wrong. It is to be corrected.
EDIT: Here is the corrected sIndex, which completes the instance:
sIndex :: forall n. KnownNat n => Symmetric n -> Integer -> Integer
sIndex xs m = let
n = toInteger (natVal (Proxy :: Proxy n))
in sIndex_ xs (m `mod` n) n
where
sIndex_ :: Symmetric m -> Integer -> Integer -> Integer
sIndex_ S1 _ _ = 0
sIndex_ (x :. _) 0 _ = cIndex x
sIndex_ (x :. xs) m n = let
i = cIndex x + sIndex_ xs (m-1) (n-1) + 1
in if n <= i then i - n else i
I also noticed that x and y were swapped in the definition of <>, which is then corrected above.
answered Jan 3 at 7:45
Dannyu NDosDannyu NDos
1,015723
add a comment |
Your Answer
StackExchange.ifUsing("editor", function () {
StackExchange.using("externalEditor", function () {
StackExchange.using("snippets", function () {
StackExchange.snippets.init();
});
});
}, "code-snippets");
StackExchange.ready(function() {
var channelOptions = {
tags: "".split(" "),
id: "1"
};
initTagRenderer("".split(" "), "".split(" "), channelOptions);
StackExchange.using("externalEditor", function() {
// Have to fire editor after snippets, if snippets enabled
if (StackExchange.settings.snippets.snippetsEnabled) {
StackExchange.using("snippets", function() {
createEditor();
});
}
else {
createEditor();
}
});
function createEditor() {
StackExchange.prepareEditor({
heartbeatType: 'answer',
autoActivateHeartbeat: false,
convertImagesToLinks: true,
noModals: true,
showLowRepImageUploadWarning: true,
reputationToPostImages: 10,
bindNavPrevention: true,
postfix: "",
imageUploader: {
brandingHtml: "Powered by u003ca class="icon-imgur-white" href="https://imgur.com/"u003eu003c/au003e",
contentPolicyHtml: "User contributions licensed under u003ca href="https://creativecommons.org/licenses/by-sa/3.0/"u003ecc by-sa 3.0 with attribution requiredu003c/au003e u003ca href="https://stackoverflow.com/legal/content-policy"u003e(content policy)u003c/au003e",
allowUrls: true
},
onDemand: true,
discardSelector: ".discard-answer"
,immediatelyShowMarkdownHelp:true
});
}
});
Sign up or log in
StackExchange.ready(function () {
StackExchange.helpers.onClickDraftSave('#login-link');
});
Sign up using Google
Sign up using Facebook
Sign up using Email and Password
Post as a guest
Required, but never shown
StackExchange.ready(
function () {
StackExchange.openid.initPostLogin('.new-post-login', 'https%3a%2f%2fstackoverflow.com%2fquestions%2f54016517%2frecursion-through-nat-kinds%23new-answer', 'question_page');
}
);
Post as a guest
Required, but never shown
1 Answer
1
active
oldest
votes
1 Answer
1
active
oldest
votes
active
oldest
votes
active
oldest
votes
A slight change of go and f solved the problem:
instance KnownNat n => Semigroup (Symmetric n) where
x <> y = go x n where
n = toInteger (natVal (Proxy :: Proxy n))
go :: forall m. Symmetric m -> [(Integer,Integer)] -> Integer -> Symmetric m
go S1 _ _ = S1
go (_ :. xs) j m = let
i = sIndex x (sIndex y (n-m))
ix = foldr f i j
in Cyclic ix :. go xs ((ix,m) :j) (m-1)
f (j,m) i = let
ix = (i - j) `mod` m - 1
in if 0 <= ix then ix else ix + m
The key idea is to introduce a dummy parameter. Also note that Cyclic was used instead of cyclic.
Unfortunately, it turns out that I did some math wrong. It is to be corrected.
EDIT: Here is the corrected sIndex, which completes the instance:
sIndex :: forall n. KnownNat n => Symmetric n -> Integer -> Integer
sIndex xs m = let
n = toInteger (natVal (Proxy :: Proxy n))
in sIndex_ xs (m `mod` n) n
where
sIndex_ :: Symmetric m -> Integer -> Integer -> Integer
sIndex_ S1 _ _ = 0
sIndex_ (x :. _) 0 _ = cIndex x
sIndex_ (x :. xs) m n = let
i = cIndex x + sIndex_ xs (m-1) (n-1) + 1
in if n <= i then i - n else i
I also noticed that x and y were swapped in the definition of <>, which is then corrected above.
answered Jan 3 at 7:45
Dannyu NDosDannyu NDos
1,015723
add a comment |
A slight change of go and f solved the problem:
instance KnownNat n => Semigroup (Symmetric n) where
x <> y = go x n where
n = toInteger (natVal (Proxy :: Proxy n))
go :: forall m. Symmetric m -> [(Integer,Integer)] -> Integer -> Symmetric m
go S1 _ _ = S1
go (_ :. xs) j m = let
i = sIndex x (sIndex y (n-m))
ix = foldr f i j
in Cyclic ix :. go xs ((ix,m) :j) (m-1)
f (j,m) i = let
ix = (i - j) `mod` m - 1
in if 0 <= ix then ix else ix + m
The key idea is to introduce a dummy parameter. Also note that Cyclic was used instead of cyclic.
Unfortunately, it turns out that I did some math wrong. It is to be corrected.
EDIT: Here is the corrected sIndex, which completes the instance:
sIndex :: forall n. KnownNat n => Symmetric n -> Integer -> Integer
sIndex xs m = let
n = toInteger (natVal (Proxy :: Proxy n))
in sIndex_ xs (m `mod` n) n
where
sIndex_ :: Symmetric m -> Integer -> Integer -> Integer
sIndex_ S1 _ _ = 0
sIndex_ (x :. _) 0 _ = cIndex x
sIndex_ (x :. xs) m n = let
i = cIndex x + sIndex_ xs (m-1) (n-1) + 1
in if n <= i then i - n else i
I also noticed that x and y were swapped in the definition of <>, which is then corrected above.
answered Jan 3 at 7:45
Dannyu NDosDannyu NDos
1,015723
add a comment |
A slight change of go and f solved the problem:
instance KnownNat n => Semigroup (Symmetric n) where
x <> y = go x n where
n = toInteger (natVal (Proxy :: Proxy n))
go :: forall m. Symmetric m -> [(Integer,Integer)] -> Integer -> Symmetric m
go S1 _ _ = S1
go (_ :. xs) j m = let
i = sIndex x (sIndex y (n-m))
ix = foldr f i j
in Cyclic ix :. go xs ((ix,m) :j) (m-1)
f (j,m) i = let
ix = (i - j) `mod` m - 1
in if 0 <= ix then ix else ix + m
The key idea is to introduce a dummy parameter. Also note that Cyclic was used instead of cyclic.
Unfortunately, it turns out that I did some math wrong. It is to be corrected.
EDIT: Here is the corrected sIndex, which completes the instance:
sIndex :: forall n. KnownNat n => Symmetric n -> Integer -> Integer
sIndex xs m = let
n = toInteger (natVal (Proxy :: Proxy n))
in sIndex_ xs (m `mod` n) n
where
sIndex_ :: Symmetric m -> Integer -> Integer -> Integer
sIndex_ S1 _ _ = 0
sIndex_ (x :. _) 0 _ = cIndex x
sIndex_ (x :. xs) m n = let
i = cIndex x + sIndex_ xs (m-1) (n-1) + 1
in if n <= i then i - n else i
I also noticed that x and y were swapped in the definition of <>, which is then corrected above.
answered Jan 3 at 7:45
Dannyu NDosDannyu NDos
1,015723
A slight change of go and f solved the problem:
instance KnownNat n => Semigroup (Symmetric n) where
x <> y = go x n where
n = toInteger (natVal (Proxy :: Proxy n))
go :: forall m. Symmetric m -> [(Integer,Integer)] -> Integer -> Symmetric m
go S1 _ _ = S1
go (_ :. xs) j m = let
i = sIndex x (sIndex y (n-m))
ix = foldr f i j
in Cyclic ix :. go xs ((ix,m) :j) (m-1)
f (j,m) i = let
ix = (i - j) `mod` m - 1
in if 0 <= ix then ix else ix + m
The key idea is to introduce a dummy parameter. Also note that Cyclic was used instead of cyclic.
Unfortunately, it turns out that I did some math wrong. It is to be corrected.
EDIT: Here is the corrected sIndex, which completes the instance:
sIndex :: forall n. KnownNat n => Symmetric n -> Integer -> Integer
sIndex xs m = let
n = toInteger (natVal (Proxy :: Proxy n))
in sIndex_ xs (m `mod` n) n
where
sIndex_ :: Symmetric m -> Integer -> Integer -> Integer
sIndex_ S1 _ _ = 0
sIndex_ (x :. _) 0 _ = cIndex x
sIndex_ (x :. xs) m n = let
i = cIndex x + sIndex_ xs (m-1) (n-1) + 1
in if n <= i then i - n else i
I also noticed that x and y were swapped in the definition of <>, which is then corrected above.
answered Jan 3 at 7:45
Dannyu NDosDannyu NDos
1,015723
edited Jan 3 at 8:18
answered Jan 3 at 7:45
Dannyu NDosDannyu NDos
1,015723
answered Jan 3 at 7:45
Dannyu NDosDannyu NDos
1,015723
answered Jan 3 at 7:45
Dannyu NDosDannyu NDos
1,015723
1,015723
add a comment |
add a comment |
Thanks for contributing an answer to Stack Overflow!
- Please be sure to answer the question. Provide details and share your research!
But avoid …
- Asking for help, clarification, or responding to other answers.
- Making statements based on opinion; back them up with references or personal experience.
To learn more, see our tips on writing great answers.
Sign up or log in
StackExchange.ready(function () {
StackExchange.helpers.onClickDraftSave('#login-link');
});
Sign up using Google
Sign up using Facebook
Sign up using Email and Password
Post as a guest
Required, but never shown
StackExchange.ready(
function () {
StackExchange.openid.initPostLogin('.new-post-login', 'https%3a%2f%2fstackoverflow.com%2fquestions%2f54016517%2frecursion-through-nat-kinds%23new-answer', 'question_page');
}
);
Post as a guest
Required, but never shown
Sign up or log in
StackExchange.ready(function () {
StackExchange.helpers.onClickDraftSave('#login-link');
});
Sign up using Google
Sign up using Facebook
Sign up using Email and Password
Post as a guest
Required, but never shown
Sign up or log in
StackExchange.ready(function () {
StackExchange.helpers.onClickDraftSave('#login-link');
});
Sign up using Google
Sign up using Facebook
Sign up using Email and Password
Post as a guest
Required, but never shown
Sign up or log in
StackExchange.ready(function () {
StackExchange.helpers.onClickDraftSave('#login-link');
});
Sign up using Google
Sign up using Facebook
Sign up using Email and Password
Sign up using Google
Sign up using Facebook
Sign up using Email and Password
Post as a guest
Required, but never shown
Required, but never shown
Required, but never shown
Required, but never shown
Required, but never shown
Required, but never shown
Required, but never shown
Required, but never shown
Required, but never shown
