Is there a way to make this type family injective?
The following type family
type family ListVariadic (as :: [Type]) (b :: Type) = (f :: Type) where
ListVariadic (a ': as) b = a -> ListVariadic as b
ListVariadic ' b = b
is visibly not injective, e.g. ListVariadic ' (a -> a) ~ ListVariadic '[a] a.
However it is very convenient to have injectivity to help type inference along, and I don't intend to use ListVariadic with its second argument being a function type.
I have come up with two workarounds, both quite unsatisfactory:
Option 1: Pass around type families that witness a left inverse to ListVariadic (through type-classes).
type family Arguments (f :: Type) :: [Type] where
Arguments (a -> b) = a ': Arguments b
Arguments b = '
type family Return (f :: Type) :: Type where
Return (a -> b) = Return b
Return b = b
class ( f ~ ListVariadic (Arguments f) (Return f) ) => VariadicIsInjective f where
instance ( f ~ ListVariadic (Arguments f) (Return f) ) => VariadicIsInjective f where
For me this eventually introduced too much complexity, having to thread these helper typeclasses throughout.
Option 2. Explicitly list all non-function types that one is going to be using, in the definition of the variadic type family:
type family ListVariadic (as :: [Type]) (b :: Type) = (f :: Type) | f -> as b where
ListVariadic (a ': as) b = a -> ListVariadic as b
ListVariadic ' () = ()
ListVariadic ' Bool = Bool
ListVariadic ' Word = Word
ListVariadic ' Int = Int
ListVariadic ' Float = Float
ListVariadic ' Double = Double
... ... ...
ListVariadic ' (a,b) = (a,b)
ListVariadic ' (a,b,c) = (a,b,c)
... ... ...
ListVariadic ' [a] = [a]
... ... ...
Then an injectivity annotation is possible and works as intended. It's obviously quite limited... and one still ends up with constraints of the form a ~ ListVariadic ' a that need to be passed around.
I was hoping there to be a way of writing the ListVariadic type family (or something fulfilling the same purpose), indicating that its second argument is not a function, and allow an injectivity annotation.
I know I am doubly in trouble, because in the provided first definition of ListVariadic, the second equation has a bare type variable on the right hand side. That's generally not allowed when checking for injectivity... but perhaps there are some clever tricks using type synonyms that can work around this problem?
haskell type-families
asked Nov 10 at 12:50
Sam Derbyshire
310128
add a comment |
The following type family
type family ListVariadic (as :: [Type]) (b :: Type) = (f :: Type) where
ListVariadic (a ': as) b = a -> ListVariadic as b
ListVariadic ' b = b
is visibly not injective, e.g. ListVariadic ' (a -> a) ~ ListVariadic '[a] a.
However it is very convenient to have injectivity to help type inference along, and I don't intend to use ListVariadic with its second argument being a function type.
I have come up with two workarounds, both quite unsatisfactory:
Option 1: Pass around type families that witness a left inverse to ListVariadic (through type-classes).
type family Arguments (f :: Type) :: [Type] where
Arguments (a -> b) = a ': Arguments b
Arguments b = '
type family Return (f :: Type) :: Type where
Return (a -> b) = Return b
Return b = b
class ( f ~ ListVariadic (Arguments f) (Return f) ) => VariadicIsInjective f where
instance ( f ~ ListVariadic (Arguments f) (Return f) ) => VariadicIsInjective f where
For me this eventually introduced too much complexity, having to thread these helper typeclasses throughout.
Option 2. Explicitly list all non-function types that one is going to be using, in the definition of the variadic type family:
type family ListVariadic (as :: [Type]) (b :: Type) = (f :: Type) | f -> as b where
ListVariadic (a ': as) b = a -> ListVariadic as b
ListVariadic ' () = ()
ListVariadic ' Bool = Bool
ListVariadic ' Word = Word
ListVariadic ' Int = Int
ListVariadic ' Float = Float
ListVariadic ' Double = Double
... ... ...
ListVariadic ' (a,b) = (a,b)
ListVariadic ' (a,b,c) = (a,b,c)
... ... ...
ListVariadic ' [a] = [a]
... ... ...
Then an injectivity annotation is possible and works as intended. It's obviously quite limited... and one still ends up with constraints of the form a ~ ListVariadic ' a that need to be passed around.
I was hoping there to be a way of writing the ListVariadic type family (or something fulfilling the same purpose), indicating that its second argument is not a function, and allow an injectivity annotation.
I know I am doubly in trouble, because in the provided first definition of ListVariadic, the second equation has a bare type variable on the right hand side. That's generally not allowed when checking for injectivity... but perhaps there are some clever tricks using type synonyms that can work around this problem?
haskell type-families
asked Nov 10 at 12:50
Sam Derbyshire
310128
Type synonyms (sans type families) are resolved before injectivity is checked, so that's not something that could help here. Also, you're not "doubly in trouble". The reason why RHS can't be a bare type variable in the first place, as far as I understand, is exactly because allowing that would always lead to non-injectivity or type-safety violations (there is one exception and you probably know of it, it's not helpful here). What you apparently want is constrained type families (doi:10.1145/3110286). Those are, regrettably, not available in Haskell at the time of writing.
– lierdakil
Nov 11 at 23:39
add a comment |
The following type family
type family ListVariadic (as :: [Type]) (b :: Type) = (f :: Type) where
ListVariadic (a ': as) b = a -> ListVariadic as b
ListVariadic ' b = b
is visibly not injective, e.g. ListVariadic ' (a -> a) ~ ListVariadic '[a] a.
However it is very convenient to have injectivity to help type inference along, and I don't intend to use ListVariadic with its second argument being a function type.
I have come up with two workarounds, both quite unsatisfactory:
Option 1: Pass around type families that witness a left inverse to ListVariadic (through type-classes).
type family Arguments (f :: Type) :: [Type] where
Arguments (a -> b) = a ': Arguments b
Arguments b = '
type family Return (f :: Type) :: Type where
Return (a -> b) = Return b
Return b = b
class ( f ~ ListVariadic (Arguments f) (Return f) ) => VariadicIsInjective f where
instance ( f ~ ListVariadic (Arguments f) (Return f) ) => VariadicIsInjective f where
For me this eventually introduced too much complexity, having to thread these helper typeclasses throughout.
Option 2. Explicitly list all non-function types that one is going to be using, in the definition of the variadic type family:
type family ListVariadic (as :: [Type]) (b :: Type) = (f :: Type) | f -> as b where
ListVariadic (a ': as) b = a -> ListVariadic as b
ListVariadic ' () = ()
ListVariadic ' Bool = Bool
ListVariadic ' Word = Word
ListVariadic ' Int = Int
ListVariadic ' Float = Float
ListVariadic ' Double = Double
... ... ...
ListVariadic ' (a,b) = (a,b)
ListVariadic ' (a,b,c) = (a,b,c)
... ... ...
ListVariadic ' [a] = [a]
... ... ...
Then an injectivity annotation is possible and works as intended. It's obviously quite limited... and one still ends up with constraints of the form a ~ ListVariadic ' a that need to be passed around.
I was hoping there to be a way of writing the ListVariadic type family (or something fulfilling the same purpose), indicating that its second argument is not a function, and allow an injectivity annotation.
I know I am doubly in trouble, because in the provided first definition of ListVariadic, the second equation has a bare type variable on the right hand side. That's generally not allowed when checking for injectivity... but perhaps there are some clever tricks using type synonyms that can work around this problem?
haskell type-families
asked Nov 10 at 12:50
Sam Derbyshire
310128
The following type family
type family ListVariadic (as :: [Type]) (b :: Type) = (f :: Type) where
ListVariadic (a ': as) b = a -> ListVariadic as b
ListVariadic ' b = b
is visibly not injective, e.g. ListVariadic ' (a -> a) ~ ListVariadic '[a] a.
However it is very convenient to have injectivity to help type inference along, and I don't intend to use ListVariadic with its second argument being a function type.
I have come up with two workarounds, both quite unsatisfactory:
Option 1: Pass around type families that witness a left inverse to ListVariadic (through type-classes).
type family Arguments (f :: Type) :: [Type] where
Arguments (a -> b) = a ': Arguments b
Arguments b = '
type family Return (f :: Type) :: Type where
Return (a -> b) = Return b
Return b = b
class ( f ~ ListVariadic (Arguments f) (Return f) ) => VariadicIsInjective f where
instance ( f ~ ListVariadic (Arguments f) (Return f) ) => VariadicIsInjective f where
For me this eventually introduced too much complexity, having to thread these helper typeclasses throughout.
Option 2. Explicitly list all non-function types that one is going to be using, in the definition of the variadic type family:
type family ListVariadic (as :: [Type]) (b :: Type) = (f :: Type) | f -> as b where
ListVariadic (a ': as) b = a -> ListVariadic as b
ListVariadic ' () = ()
ListVariadic ' Bool = Bool
ListVariadic ' Word = Word
ListVariadic ' Int = Int
ListVariadic ' Float = Float
ListVariadic ' Double = Double
... ... ...
ListVariadic ' (a,b) = (a,b)
ListVariadic ' (a,b,c) = (a,b,c)
... ... ...
ListVariadic ' [a] = [a]
... ... ...
Then an injectivity annotation is possible and works as intended. It's obviously quite limited... and one still ends up with constraints of the form a ~ ListVariadic ' a that need to be passed around.
I was hoping there to be a way of writing the ListVariadic type family (or something fulfilling the same purpose), indicating that its second argument is not a function, and allow an injectivity annotation.
I know I am doubly in trouble, because in the provided first definition of ListVariadic, the second equation has a bare type variable on the right hand side. That's generally not allowed when checking for injectivity... but perhaps there are some clever tricks using type synonyms that can work around this problem?
haskell type-families
haskell type-families
asked Nov 10 at 12:50
Sam Derbyshire
310128
asked Nov 10 at 12:50
Sam Derbyshire
310128
edited Nov 11 at 11:42
asked Nov 10 at 12:50
Sam Derbyshire
310128
asked Nov 10 at 12:50
Sam Derbyshire
310128
asked Nov 10 at 12:50
Sam Derbyshire
310128
310128
Type synonyms (sans type families) are resolved before injectivity is checked, so that's not something that could help here. Also, you're not "doubly in trouble". The reason why RHS can't be a bare type variable in the first place, as far as I understand, is exactly because allowing that would always lead to non-injectivity or type-safety violations (there is one exception and you probably know of it, it's not helpful here). What you apparently want is constrained type families (doi:10.1145/3110286). Those are, regrettably, not available in Haskell at the time of writing.
– lierdakil
Nov 11 at 23:39
add a comment |
Type synonyms (sans type families) are resolved before injectivity is checked, so that's not something that could help here. Also, you're not "doubly in trouble". The reason why RHS can't be a bare type variable in the first place, as far as I understand, is exactly because allowing that would always lead to non-injectivity or type-safety violations (there is one exception and you probably know of it, it's not helpful here). What you apparently want is constrained type families (doi:10.1145/3110286). Those are, regrettably, not available in Haskell at the time of writing.
– lierdakil
Nov 11 at 23:39
Type synonyms (sans type families) are resolved before injectivity is checked, so that's not something that could help here. Also, you're not "doubly in trouble". The reason why RHS can't be a bare type variable in the first place, as far as I understand, is exactly because allowing that would always lead to non-injectivity or type-safety violations (there is one exception and you probably know of it, it's not helpful here). What you apparently want is constrained type families (doi:10.1145/3110286). Those are, regrettably, not available in Haskell at the time of writing.
– lierdakil
Nov 11 at 23:39
Type synonyms (sans type families) are resolved before injectivity is checked, so that's not something that could help here. Also, you're not "doubly in trouble". The reason why RHS can't be a bare type variable in the first place, as far as I understand, is exactly because allowing that would always lead to non-injectivity or type-safety violations (there is one exception and you probably know of it, it's not helpful here). What you apparently want is constrained type families (doi:10.1145/3110286). Those are, regrettably, not available in Haskell at the time of writing.
– lierdakil
Nov 11 at 23:39
add a comment |
active
oldest
votes
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%2f53239120%2fis-there-a-way-to-make-this-type-family-injective%23new-answer', 'question_page');
}
);
Post as a guest
Required, but never shown
active
oldest
votes
active
oldest
votes
active
oldest
votes
active
oldest
votes
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.
Some of your past answers have not been well-received, and you're in danger of being blocked from answering.
Please pay close attention to the following guidance:
- 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%2f53239120%2fis-there-a-way-to-make-this-type-family-injective%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
Type synonyms (sans type families) are resolved before injectivity is checked, so that's not something that could help here. Also, you're not "doubly in trouble". The reason why RHS can't be a bare type variable in the first place, as far as I understand, is exactly because allowing that would always lead to non-injectivity or type-safety violations (there is one exception and you probably know of it, it's not helpful here). What you apparently want is constrained type families (doi:10.1145/3110286). Those are, regrettably, not available in Haskell at the time of writing.
– lierdakil
Nov 11 at 23:39