Boxing (Day) Question
As I understand it, with unboxing switched on (->) actually has this kind: (->) :: ? -> ? -> * Reading the Core specification, GHC has a particular kind of "polykindism" which introduces kind "?", and defines specialisation such that "?" may be replaced by "*" or "#" inside any kind. Accordingly, (->) may be specialised: (->) :: * -> * -> * (->) :: # -> * -> * (->) :: * -> # -> * (->) :: # -> # -> * Examples: module Boxing where import GHC.Exts fooSS :: (->) Int Int fooSS 3 = 5 fooSS _ = 2 fooHS :: (->) Int# Int fooHS 3# = 5 fooHS _ = 2 fooSH :: (->) Int Int# fooSH 3 = 5# fooSH _ = 2# fooHH :: (->) Int# Int# fooHH 3# = 5# fooHH _ = 2# type Fun = (->) fooHH' :: Fun Int# Int# fooHH' 3# = 5# fooHH' _ = 2# Do any other type constructors or symbols have a kind with "?" in it? I like the "kind" approach to unboxed types. It automatically rules out "[Int#]" by kind mismatch, for instance. But I was disappointed I couldn't do this with GHC 6.4.1: data MyC s = MkMyC (s Int# Int) or class C s where c :: s Int# Int (in either case: "Kind error: Expecting kind `k_a19o', but `Int#' has kind `#' In the class declaration for `C'") There's no kind mismatch here, merely a restriction that the kinds of arguments to classes be #-free. I can't do this, either: newtype MyD (u :: #) = MkMyD (u -> Bool) GHC actually complains about parsing the kind signature. Would Bad Things Happen if this restriction were lifted? I don't have a pressing need for it actually, though this might be useful: class Boxed (b :: *) (u :: #) | b -> u, u -> b where box :: u -> b unbox :: b -> u In case you're worried, lifting the restriction would NOT allow uncompilable things such as newtype MyE (u :: #) = MkMyE u ...simply because there's already a straightforward restriction that values in type constructors have types of kind "*". It is merely the notion of "#-freeness" that seems unnecessary. It would, however, allow this: newtype Box (u :: #) = MkBox (() -> u) ...and quite possibly this: newtype Value (x :: ?) = MkValue (() -> x) I believe these can be compiled safely? -- Ashley Yakeley, Seattle WA
On the whole it looks like you want type variables with kind #. There are very good implementation reasons for not allowing this. If you had type variables of kind # you could have polymorphic functions over unboxed values. But since the values are unboxed they don't have a uniform representation (e.g., a Double# is probably twice the size of a Float#). So polymorphic functions over unboxed values are not easy to implement. (You can imagine implementations of them, but none of them are pleasent.) -- Lennart Ashley Yakeley wrote:
As I understand it, with unboxing switched on (->) actually has this kind:
(->) :: ? -> ? -> *
Reading the Core specification, GHC has a particular kind of "polykindism" which introduces kind "?", and defines specialisation such that "?" may be replaced by "*" or "#" inside any kind. Accordingly, (->) may be specialised:
(->) :: * -> * -> * (->) :: # -> * -> * (->) :: * -> # -> * (->) :: # -> # -> *
Examples:
module Boxing where import GHC.Exts
fooSS :: (->) Int Int fooSS 3 = 5 fooSS _ = 2
fooHS :: (->) Int# Int fooHS 3# = 5 fooHS _ = 2
fooSH :: (->) Int Int# fooSH 3 = 5# fooSH _ = 2#
fooHH :: (->) Int# Int# fooHH 3# = 5# fooHH _ = 2#
type Fun = (->)
fooHH' :: Fun Int# Int# fooHH' 3# = 5# fooHH' _ = 2#
Do any other type constructors or symbols have a kind with "?" in it?
I like the "kind" approach to unboxed types. It automatically rules out "[Int#]" by kind mismatch, for instance. But I was disappointed I couldn't do this with GHC 6.4.1:
data MyC s = MkMyC (s Int# Int)
or
class C s where c :: s Int# Int
(in either case: "Kind error: Expecting kind `k_a19o', but `Int#' has kind `#' In the class declaration for `C'")
There's no kind mismatch here, merely a restriction that the kinds of arguments to classes be #-free. I can't do this, either:
newtype MyD (u :: #) = MkMyD (u -> Bool)
GHC actually complains about parsing the kind signature.
Would Bad Things Happen if this restriction were lifted? I don't have a pressing need for it actually, though this might be useful:
class Boxed (b :: *) (u :: #) | b -> u, u -> b where box :: u -> b unbox :: b -> u
In case you're worried, lifting the restriction would NOT allow uncompilable things such as
newtype MyE (u :: #) = MkMyE u
...simply because there's already a straightforward restriction that values in type constructors have types of kind "*". It is merely the notion of "#-freeness" that seems unnecessary. It would, however, allow this:
newtype Box (u :: #) = MkBox (() -> u)
...and quite possibly this:
newtype Value (x :: ?) = MkValue (() -> x)
I believe these can be compiled safely?
In article <43AFCA38.5000302@augustsson.net>, Lennart Augustsson <lennart@augustsson.net> wrote:
On the whole it looks like you want type variables with kind #. There are very good implementation reasons for not allowing this. If you had type variables of kind # you could have polymorphic functions over unboxed values. But since the values are unboxed they don't have a uniform representation (e.g., a Double# is probably twice the size of a Float#). So polymorphic functions over unboxed values are not easy to implement. (You can imagine implementations of them, but none of them are pleasent.)
Oh, I hadn't thought of that. One solution might be to have a kind for each kind of storage: * for boxed values #4 for 4-byte values #8 for 8-byte values #P for pointers to things that need to be GC'd (or whatever) etc. Do you think this would work? -- Ashley Yakeley, Seattle WA
Hello Ashley, Monday, December 26, 2005, 2:41:38 PM, you wrote:
On the whole it looks like you want type variables with kind #. There are very good implementation reasons for not allowing this. If you had type variables of kind # you could have polymorphic functions over unboxed values. But since the values are unboxed they don't have a uniform representation (e.g., a Double# is probably twice the size of a Float#). So polymorphic functions over unboxed values are not easy to implement. (You can imagine implementations of them, but none of them are pleasent.)
AY> Oh, I hadn't thought of that. AY> One solution might be to have a kind for each kind of storage: AY> * for boxed values AY> #4 for 4-byte values AY> #8 for 8-byte values AY> #P for pointers to things that need to be GC'd (or whatever) AY> etc. AY> Do you think this would work? it's unserious :) overloading of unboxed types must be resolved at compile time, as in C++ templates. Haskell polymorhism, based on using of type classes, oriented to run-time resolving of polymorphic usage, although SPECIALIZE/INLINE/RULES pragmas can optimize code, the program must remain correct without these pragmas and therefore overloading is limited to boxed types. aside of different sizes, boxed values carry dictionaries used to run-time resolving of overloaded functions. where unboxed value must hide this dictionary? :) but i'm totally agree that we must have C++-like compile-time overloading in order to create fast programs -- Best regards, Bulat mailto:bulatz@HotPOP.com
In article <155148271993.20051226161427@HotPOP.com>, Bulat Ziganshin <bulatz@HotPOP.com> wrote:
it's unserious :) overloading of unboxed types must be resolved at compile time, as in C++ templates.
Why can't (->) that's been specialised to #4 -> #4 -> * just generate a function that takes an anonymous 4-byte quantity and returns an anonymous 4-byte quantity?
Haskell polymorhism, based on using of type classes, oriented to run-time resolving of polymorphic usage, although SPECIALIZE/INLINE/RULES pragmas can optimize code, the program must remain correct without these pragmas and therefore overloading is limited to boxed types. aside of different sizes, boxed values carry dictionaries used to run-time resolving of overloaded functions. where unboxed value must hide this dictionary? :)
I thought functions receive dictionaries, rather than dictionaries being stored inside values? For instance: class C (x :: #4) where ... foo :: (C x) => x -> Bool foo x = ... might be generate something like this: HsBool foo (CDict dict,int32 x) { ... }
but i'm totally agree that we must have C++-like compile-time overloading in order to create fast programs
-- Ashley Yakeley, Seattle WA
Hello Ashley, Tuesday, December 27, 2005, 2:46:11 AM, you wrote:
it's unserious :) overloading of unboxed types must be resolved at compile time, as in C++ templates.
Why can't (->>) that's been specialised to #4 -> #4 -> * just generate a AY> function that takes an anonymous 4-byte quantity and returns an AY> anonymous 4-byte quantity? for why? AY> class C (x :: #4) where ... AY> foo :: (C x) => x -> Bool AY> foo x = ... AY> might be generate something like this: AY> HsBool foo (CDict dict,int32 x) { ... } yes, it can be implemented in such way. but i don't see any interesting usage for this compile+run-time overloading resolution mandatory compile-time overloading have many much benefits, because it allows to inline used procedures and futher optimize code. something like this is done in jhc C++ just supports both types of overloading through a different synax forms (templates and virtual methods). i'm interested in having option to force Haskell compiler use compile-time overloading and fail compilation if that is impossible for some reason; but at the same time use the same syntax forms for both overloading types adding facility to specify strictness of arguments and function result can help compiler to decide whether arguments/result can be unboxed -- Best regards, Bulat mailto:bulatz@HotPOP.com
On 12/26/05, Ashley Yakeley <ashley@semantic.org> wrote:
I thought functions receive dictionaries, rather than dictionaries being stored inside values? For instance:
class C (x :: #4) where ...
foo :: (C x) => x -> Bool foo x = ...
might be generate something like this:
HsBool foo (CDict dict,int32 x) { ... }
Just a strange thought, but what about... foo :: x# -> ... => ... foo (void *x, ...) { ... } Just because it's unboxed doesn't mean it isn't in memory... -- Taral <taralx@gmail.com> "Computer science is no more about computers than astronomy is about telescopes." -- Edsger Dijkstra
Taral wrote:
Just a strange thought, but what about...
foo :: x# -> ... => ... foo (void *x, ...) { ... }
Just because it's unboxed doesn't mean it isn't in memory...
Then you have to worry about garbage collection. That's OK, but that would be a separate kind, pointers to unboxed values that the garbage collector can reclaim. But we might also want literals. The idea is to do C in Haskell, but with better typing. We separate out the storage aspects of C types as kinds, while leaving the semantics as types. One could add various kinds of "polykindism", which would mostly end up as compile-time overloading (or inlined) similar to C++ templates. For instance: (#,#) :: #m -> #n -> #m+n I'm not really sure how much demand there is for it, mind, given the possible degree of complexity involved in doing it right. -- Ashley Yakeley
Ashley Yakeley wrote:
In article <43AFCA38.5000302@augustsson.net>, Lennart Augustsson <lennart@augustsson.net> wrote:
On the whole it looks like you want type variables with kind #. There are very good implementation reasons for not allowing this. If you had type variables of kind # you could have polymorphic functions over unboxed values. But since the values are unboxed they don't have a uniform representation (e.g., a Double# is probably twice the size of a Float#). So polymorphic functions over unboxed values are not easy to implement. (You can imagine implementations of them, but none of them are pleasent.)
Oh, I hadn't thought of that.
One solution might be to have a kind for each kind of storage:
* for boxed values #4 for 4-byte values #8 for 8-byte values #P for pointers to things that need to be GC'd (or whatever) etc.
Do you think this would work?
Yes, I think it would work. But I'd think it would be awkward. Now you need to know the size of each unboxed type to make polymorphic functions (and that's not even portable). -- Lennart
In article <43B0962E.6070201@augustsson.net>, Lennart Augustsson <lennart@augustsson.net> wrote:
Yes, I think it would work. But I'd think it would be awkward. Now you need to know the size of each unboxed type to make polymorphic functions (and that's not even portable).
Yes, your polymorphic types and functions are limited to a particular kind of storage. But it's similar to C in this respect. If you wanted to do allocation yourself, for instance, you could use typed pointers, which would all have the same kind. This could be an alternative way of doing FFI. It also might be interesting to allow user definition of certain kinds of unboxed datatypes, similar to C++ enumerations. -- Ashley Yakeley, Seattle WA
On the whole it looks like you want type variables with kind #. There are very good implementation reasons for not allowing this. If you had type variables of kind # you could have polymorphic functions over unboxed values. But since the values are unboxed they don't have a uniform representation (e.g., a Double# is probably twice the size of a Float#). So polymorphic functions over unboxed values are not easy to implement. (You can imagine implementations of them, but none of them are pleasent.)
That reminds me of something that I have wondered about for some time. Why is there such reluctance to instantiate polymorhic functions with the types with which they are used? (This isn't done automatically in complilers right?) I can imagine that it is akward to delay code generation until all uses of a function are known, and that in some cases there may be infinitely many instances needed. But apart from that, what are the reasons against this implementation technique? /Niklas
On Mon, Dec 26, 2005 at 02:22:57PM +0100, Niklas Sorensson wrote:
That reminds me of something that I have wondered about for some time. Why is there such reluctance to instantiate polymorhic functions with the types with which they are used? (This isn't done automatically in complilers right?)
I can imagine that it is akward to delay code generation until all uses of a function are known, and that in some cases there may be infinitely many instances needed. But apart from that, what are the reasons against this implementation technique?
What made you think that this technique isn't used? It is used in GHC. However, there are cases where it can't be used, most notably with polymorphic recursion, existential types or higher-rank polymorphism. Best regards Tomasz -- I am searching for a programmer who is good at least in some of [Haskell, ML, C++, Linux, FreeBSD, math] for work in Warsaw, Poland
I can imagine that it is akward to delay code generation until all uses of a function are known, and that in some cases there may be infinitely many instances needed. But apart from that, what are the reasons against this implementation technique?
What made you think that this technique isn't used?
I'm not sure. It seems I didn't hear it from any official sources at least :)
It is used in GHC. However, there are cases where it can't be used, most notably with polymorphic recursion, existential types or higher-rank polymorphism.
That's what I thought. But I'm still curious when it is used, and why it isn't a suitable solution for unboxed polymorhic functions in most cases. /Niklas
On Mon, Dec 26, 2005 at 06:45:09PM +0100, Niklas Sorensson wrote:
That's what I thought. But I'm still curious when it is used, and why it isn't a suitable solution for unboxed polymorhic functions in most cases.
I always thought A nice extension would be to allow polymorphic functions that are {-# INLINE #-}'d for which all polymorphic functions called by it are also inlined to be applied to unboxed arguments. a $ b = a b id x = x f . g = \x -> f (g x) being particularly useful instances of this John -- John Meacham - ⑆repetae.net⑆john⑈
Niklas Sorensson wrote:
That's what I thought. But I'm still curious when it is used, and why it isn't a suitable solution for unboxed polymorhic functions in most cases.
But getting most cases right isn't enough, you have to get all cases right. So if you want to have unboxed polymorphic functions you need to handle the general case. And that's the ugly part. -- Lennart
participants (7)
-
Ashley Yakeley -
Bulat Ziganshin -
John Meacham -
Lennart Augustsson -
Niklas Sorensson -
Taral -
Tomasz Zielonka