Constructing a Nat type
I'm currently learning about using Nat from GHC.TypeLits
I am trying to lift an integer to the type level for testing via these definitions:
type IntNat (t::Nat) = Int
incNat :: IntNat t -> IntNat (t + 1)
incNat n = n + 1
fromInt :: Int -> IntNat t
fromInt(0) = (0 :: IntNat 0)
fromInt(n) = incNat (fromInt(n-1))
four = fromInt 4
From my understanding this should result in:
four = 4 :: IntNat (Nat 4)
However I am getting:
four = 4 :: IntNat t
Where am I going wrong, is it just that fromInt is erasing the type information?
haskell types
asked Jan 3 at 18:15
Cjen1Cjen1
9351733
add a comment |
I'm currently learning about using Nat from GHC.TypeLits
I am trying to lift an integer to the type level for testing via these definitions:
type IntNat (t::Nat) = Int
incNat :: IntNat t -> IntNat (t + 1)
incNat n = n + 1
fromInt :: Int -> IntNat t
fromInt(0) = (0 :: IntNat 0)
fromInt(n) = incNat (fromInt(n-1))
four = fromInt 4
From my understanding this should result in:
four = 4 :: IntNat (Nat 4)
However I am getting:
four = 4 :: IntNat t
Where am I going wrong, is it just that fromInt is erasing the type information?
haskell types
asked Jan 3 at 18:15
Cjen1Cjen1
9351733
1
I doubt thatfromIntcompiles. Could you produce an MCVE to show your problem?
– AJFarmar
Jan 3 at 18:27
1
According to your definitionIntNat t = Intfor allt. Your signatures are exactly equivalent toincNat :: Int->IntandfromInt :: Int->Int.fourhas typesIntNat (Nat 0), IntNat (Nat 1), ..., all of them actually beingInt. For some reason, the type inference engine prefer the formIntNat t, as if it were the most general type (it is, but so are all the others). Note that, crucially, you are using a type synonym and not anewtype.
– chi
Jan 3 at 18:35
1
It is quite clear thatfromInt :: Int -> IntNat tso any time you apply it to a value of type Int you will get a value of typeIntNat t. You seem to be wanting dependent types.
– Thomas M. DuBuisson
Jan 3 at 18:52
add a comment |
I'm currently learning about using Nat from GHC.TypeLits
I am trying to lift an integer to the type level for testing via these definitions:
type IntNat (t::Nat) = Int
incNat :: IntNat t -> IntNat (t + 1)
incNat n = n + 1
fromInt :: Int -> IntNat t
fromInt(0) = (0 :: IntNat 0)
fromInt(n) = incNat (fromInt(n-1))
four = fromInt 4
From my understanding this should result in:
four = 4 :: IntNat (Nat 4)
However I am getting:
four = 4 :: IntNat t
Where am I going wrong, is it just that fromInt is erasing the type information?
haskell types
asked Jan 3 at 18:15
Cjen1Cjen1
9351733
I'm currently learning about using Nat from GHC.TypeLits
I am trying to lift an integer to the type level for testing via these definitions:
type IntNat (t::Nat) = Int
incNat :: IntNat t -> IntNat (t + 1)
incNat n = n + 1
fromInt :: Int -> IntNat t
fromInt(0) = (0 :: IntNat 0)
fromInt(n) = incNat (fromInt(n-1))
four = fromInt 4
From my understanding this should result in:
four = 4 :: IntNat (Nat 4)
However I am getting:
four = 4 :: IntNat t
Where am I going wrong, is it just that fromInt is erasing the type information?
haskell types
haskell types
asked Jan 3 at 18:15
Cjen1Cjen1
9351733
asked Jan 3 at 18:15
Cjen1Cjen1
9351733
asked Jan 3 at 18:15
Cjen1Cjen1
9351733
asked Jan 3 at 18:15
Cjen1Cjen1
9351733
asked Jan 3 at 18:15
Cjen1Cjen1
9351733
9351733
1
I doubt thatfromIntcompiles. Could you produce an MCVE to show your problem?
– AJFarmar
Jan 3 at 18:27
1
According to your definitionIntNat t = Intfor allt. Your signatures are exactly equivalent toincNat :: Int->IntandfromInt :: Int->Int.fourhas typesIntNat (Nat 0), IntNat (Nat 1), ..., all of them actually beingInt. For some reason, the type inference engine prefer the formIntNat t, as if it were the most general type (it is, but so are all the others). Note that, crucially, you are using a type synonym and not anewtype.
– chi
Jan 3 at 18:35
1
It is quite clear thatfromInt :: Int -> IntNat tso any time you apply it to a value of type Int you will get a value of typeIntNat t. You seem to be wanting dependent types.
– Thomas M. DuBuisson
Jan 3 at 18:52
add a comment |
1
I doubt thatfromIntcompiles. Could you produce an MCVE to show your problem?
– AJFarmar
Jan 3 at 18:27
1
According to your definitionIntNat t = Intfor allt. Your signatures are exactly equivalent toincNat :: Int->IntandfromInt :: Int->Int.fourhas typesIntNat (Nat 0), IntNat (Nat 1), ..., all of them actually beingInt. For some reason, the type inference engine prefer the formIntNat t, as if it were the most general type (it is, but so are all the others). Note that, crucially, you are using a type synonym and not anewtype.
– chi
Jan 3 at 18:35
1
It is quite clear thatfromInt :: Int -> IntNat tso any time you apply it to a value of type Int you will get a value of typeIntNat t. You seem to be wanting dependent types.
– Thomas M. DuBuisson
Jan 3 at 18:52
1
1
I doubt that
fromInt compiles. Could you produce an MCVE to show your problem?– AJFarmar
Jan 3 at 18:27
I doubt that
fromInt compiles. Could you produce an MCVE to show your problem?– AJFarmar
Jan 3 at 18:27
1
1
According to your definition
IntNat t = Int for all t. Your signatures are exactly equivalent to incNat :: Int->Int and fromInt :: Int->Int. four has types IntNat (Nat 0), IntNat (Nat 1), ..., all of them actually being Int. For some reason, the type inference engine prefer the form IntNat t, as if it were the most general type (it is, but so are all the others). Note that, crucially, you are using a type synonym and not a newtype.– chi
Jan 3 at 18:35
According to your definition
IntNat t = Int for all t. Your signatures are exactly equivalent to incNat :: Int->Int and fromInt :: Int->Int. four has types IntNat (Nat 0), IntNat (Nat 1), ..., all of them actually being Int. For some reason, the type inference engine prefer the form IntNat t, as if it were the most general type (it is, but so are all the others). Note that, crucially, you are using a type synonym and not a newtype.– chi
Jan 3 at 18:35
1
1
It is quite clear that
fromInt :: Int -> IntNat t so any time you apply it to a value of type Int you will get a value of type IntNat t. You seem to be wanting dependent types.– Thomas M. DuBuisson
Jan 3 at 18:52
It is quite clear that
fromInt :: Int -> IntNat t so any time you apply it to a value of type Int you will get a value of type IntNat t. You seem to be wanting dependent types.– Thomas M. DuBuisson
Jan 3 at 18:52
add a comment |
1 Answer
1
active
oldest
votes
Because you defined a type synonym, and not a newtype, the meaning is quite different than what you seem to think. Roughly, IntNat _ will unify with Int and thus any other IntNat _.
You can try this out by defining other intnats and see them unify in, say, a list:
*Main> let five = 5 :: IntNat 99
*Main> let xs = [four, five] :: [IntNat 42]
*Main> :t xs
xs :: [IntNat 42]
or using a single intnat:
*Main> let four' = four :: IntNat 1000
*Main> :t four'
four' :: IntNat 1000
Instead consider using a newtype, such as newtype IntNat (n :: Nat) = IN Int. You'd get an error like:
• Couldn't match type ‘t’ with ‘0’
‘t’ is a rigid type variable bound by
the type signature for:
fromInt :: forall (t :: Nat). Int -> IntNat t
at so.hs:12:1-26
Expected type: IntNat t
Actual type: IntNat 0
• In the expression: IN 0 :: IntNat 0
In an equation for ‘fromInt’: fromInt 0 = IN 0 :: IntNat 0
• Relevant bindings include
fromInt :: Int -> IntNat t (bound at so.hs:13:1)
This is because t and 0 are not the same - t is universal not existential. The offending lines are:
fromInt :: Int -> IntNat t
fromInt 0 = 0 :: IntNat 0
forall t. t == 0 is a hard proof to write
answered Jan 3 at 20:56
Thomas M. DuBuissonThomas M. DuBuisson
56.1k690154
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%2f54027671%2fconstructing-a-nat-type%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
Because you defined a type synonym, and not a newtype, the meaning is quite different than what you seem to think. Roughly, IntNat _ will unify with Int and thus any other IntNat _.
You can try this out by defining other intnats and see them unify in, say, a list:
*Main> let five = 5 :: IntNat 99
*Main> let xs = [four, five] :: [IntNat 42]
*Main> :t xs
xs :: [IntNat 42]
or using a single intnat:
*Main> let four' = four :: IntNat 1000
*Main> :t four'
four' :: IntNat 1000
Instead consider using a newtype, such as newtype IntNat (n :: Nat) = IN Int. You'd get an error like:
• Couldn't match type ‘t’ with ‘0’
‘t’ is a rigid type variable bound by
the type signature for:
fromInt :: forall (t :: Nat). Int -> IntNat t
at so.hs:12:1-26
Expected type: IntNat t
Actual type: IntNat 0
• In the expression: IN 0 :: IntNat 0
In an equation for ‘fromInt’: fromInt 0 = IN 0 :: IntNat 0
• Relevant bindings include
fromInt :: Int -> IntNat t (bound at so.hs:13:1)
This is because t and 0 are not the same - t is universal not existential. The offending lines are:
fromInt :: Int -> IntNat t
fromInt 0 = 0 :: IntNat 0
forall t. t == 0 is a hard proof to write
answered Jan 3 at 20:56
Thomas M. DuBuissonThomas M. DuBuisson
56.1k690154
add a comment |
Because you defined a type synonym, and not a newtype, the meaning is quite different than what you seem to think. Roughly, IntNat _ will unify with Int and thus any other IntNat _.
You can try this out by defining other intnats and see them unify in, say, a list:
*Main> let five = 5 :: IntNat 99
*Main> let xs = [four, five] :: [IntNat 42]
*Main> :t xs
xs :: [IntNat 42]
or using a single intnat:
*Main> let four' = four :: IntNat 1000
*Main> :t four'
four' :: IntNat 1000
Instead consider using a newtype, such as newtype IntNat (n :: Nat) = IN Int. You'd get an error like:
• Couldn't match type ‘t’ with ‘0’
‘t’ is a rigid type variable bound by
the type signature for:
fromInt :: forall (t :: Nat). Int -> IntNat t
at so.hs:12:1-26
Expected type: IntNat t
Actual type: IntNat 0
• In the expression: IN 0 :: IntNat 0
In an equation for ‘fromInt’: fromInt 0 = IN 0 :: IntNat 0
• Relevant bindings include
fromInt :: Int -> IntNat t (bound at so.hs:13:1)
This is because t and 0 are not the same - t is universal not existential. The offending lines are:
fromInt :: Int -> IntNat t
fromInt 0 = 0 :: IntNat 0
forall t. t == 0 is a hard proof to write
answered Jan 3 at 20:56
Thomas M. DuBuissonThomas M. DuBuisson
56.1k690154
add a comment |
Because you defined a type synonym, and not a newtype, the meaning is quite different than what you seem to think. Roughly, IntNat _ will unify with Int and thus any other IntNat _.
You can try this out by defining other intnats and see them unify in, say, a list:
*Main> let five = 5 :: IntNat 99
*Main> let xs = [four, five] :: [IntNat 42]
*Main> :t xs
xs :: [IntNat 42]
or using a single intnat:
*Main> let four' = four :: IntNat 1000
*Main> :t four'
four' :: IntNat 1000
Instead consider using a newtype, such as newtype IntNat (n :: Nat) = IN Int. You'd get an error like:
• Couldn't match type ‘t’ with ‘0’
‘t’ is a rigid type variable bound by
the type signature for:
fromInt :: forall (t :: Nat). Int -> IntNat t
at so.hs:12:1-26
Expected type: IntNat t
Actual type: IntNat 0
• In the expression: IN 0 :: IntNat 0
In an equation for ‘fromInt’: fromInt 0 = IN 0 :: IntNat 0
• Relevant bindings include
fromInt :: Int -> IntNat t (bound at so.hs:13:1)
This is because t and 0 are not the same - t is universal not existential. The offending lines are:
fromInt :: Int -> IntNat t
fromInt 0 = 0 :: IntNat 0
forall t. t == 0 is a hard proof to write
answered Jan 3 at 20:56
Thomas M. DuBuissonThomas M. DuBuisson
56.1k690154
Because you defined a type synonym, and not a newtype, the meaning is quite different than what you seem to think. Roughly, IntNat _ will unify with Int and thus any other IntNat _.
You can try this out by defining other intnats and see them unify in, say, a list:
*Main> let five = 5 :: IntNat 99
*Main> let xs = [four, five] :: [IntNat 42]
*Main> :t xs
xs :: [IntNat 42]
or using a single intnat:
*Main> let four' = four :: IntNat 1000
*Main> :t four'
four' :: IntNat 1000
Instead consider using a newtype, such as newtype IntNat (n :: Nat) = IN Int. You'd get an error like:
• Couldn't match type ‘t’ with ‘0’
‘t’ is a rigid type variable bound by
the type signature for:
fromInt :: forall (t :: Nat). Int -> IntNat t
at so.hs:12:1-26
Expected type: IntNat t
Actual type: IntNat 0
• In the expression: IN 0 :: IntNat 0
In an equation for ‘fromInt’: fromInt 0 = IN 0 :: IntNat 0
• Relevant bindings include
fromInt :: Int -> IntNat t (bound at so.hs:13:1)
This is because t and 0 are not the same - t is universal not existential. The offending lines are:
fromInt :: Int -> IntNat t
fromInt 0 = 0 :: IntNat 0
forall t. t == 0 is a hard proof to write
answered Jan 3 at 20:56
Thomas M. DuBuissonThomas M. DuBuisson
56.1k690154
answered Jan 3 at 20:56
Thomas M. DuBuissonThomas M. DuBuisson
56.1k690154
answered Jan 3 at 20:56
Thomas M. DuBuissonThomas M. DuBuisson
56.1k690154
answered Jan 3 at 20:56
Thomas M. DuBuissonThomas M. DuBuisson
56.1k690154
56.1k690154
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%2f54027671%2fconstructing-a-nat-type%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
1
I doubt that
fromIntcompiles. Could you produce an MCVE to show your problem?– AJFarmar
Jan 3 at 18:27
1
According to your definition
IntNat t = Intfor allt. Your signatures are exactly equivalent toincNat :: Int->IntandfromInt :: Int->Int.fourhas typesIntNat (Nat 0), IntNat (Nat 1), ..., all of them actually beingInt. For some reason, the type inference engine prefer the formIntNat t, as if it were the most general type (it is, but so are all the others). Note that, crucially, you are using a type synonym and not anewtype.– chi
Jan 3 at 18:35
1
It is quite clear that
fromInt :: Int -> IntNat tso any time you apply it to a value of type Int you will get a value of typeIntNat t. You seem to be wanting dependent types.– Thomas M. DuBuisson
Jan 3 at 18:52