5 ms·

That's a really beautiful article! Using kinds to keep track of the concrete representation of a reference to a type (rather than the concrete representation o

by fmap 8y ago

That's a really beautiful article! Using kinds to keep track of the concrete representation of a reference to a type (rather than the concrete representation of the type itself) is one of the real gems in GHCs design. However, one problem with it is that a polymorphic type, such as [] of kind "* -> *", or a function like map of type "forall a b. (a -> b) -> [a] -> [b]" really only works with boxed types. I always wondered how expensive it would be to monomorphize everything at the level of kinds and have what GHC calls levity polymorphism by default. Languages like Rust and C++ always monomorphize everything and while this does get slow it is still not the exponential blowup that theory suggests. In fact, there is an ML compiler (MLton) which does the same and it is still not too bad. Doing it at the level of reference representation - which is where the generated code actually needs to change - should be much cheaper and definitely a practical default. The only real problem I see is that you could in principle write code that does "kind polymorphic" recursion, which couldn't be compiled away. But that sounds seriously crazy and I see no reason to allow it in the first place...

lmm 8y ago
> The only real problem I see is that you could in principle write code that does "kind polymorphic" recursion, which couldn't be compiled away. But that sounds seriously crazy and I see no reason to allow it in the first place... Wouldn't you want kind-polymorphic recursion for implementing recursion-schemes like patterns at the type level?
Athas 8y ago
> However, one problem with it is that a polymorphic type, such as [] of kind "* -> ", or a function like map of type "forall a b. (a -> b) -> [a] -> [b]" really only works with boxed types. Can you explain why this is, or provide a reference to literature where it was investigated? I still (even after getting a PhD in compiling functional languages!) do not understand why you could not create code parameterised over the sizes of the arguments. For example, a 'cons' cell could be represented as first the size of the 'car' in bytes, then the 'car' value inline/unboxed, then a pointer to the 'cdr' cell. The Sixten language[0] does this, although it's still very early in its development. I'm not saying this is necessarily a good solution, I just wonder why I have never seen it seriously considered (and perhaps rejected). In practice, I do believe that monomorphisation is very often a good strategy. [0]: https://github.com/ollef/sixten https://github.com/ollef/sixten
- gpderetta 8y ago
  > why you could not create code parameterised over the sizes of the arguments If I understand correctly, that's what BitC was trying to do, but the extreme complexity of the compilation model was cited as one of the reasons the project failed. The postmortem is here I think, but I can't access it right now: http://www.coyotos.org/pipermail/bitc-dev/2012-March/003300.html http://www.coyotos.org/pipermail/bitc-dev/2012-March/003300....

by fmap 8y ago

lmm 8y ago

> The only real problem I see is that you could in principle write code that does "kind polymorphic" recursion, which couldn't be compiled away. But that sounds seriously crazy and I see no reason to allow it in the first place... Wouldn't you want kind-polymorphic recursion for implementing recursion-schemes like patterns at the type level?

Athas 8y ago

> However, one problem with it is that a polymorphic type, such as [] of kind "* -> ", or a function like map of type "forall a b. (a -> b) -> [a] -> [b]" really only works with boxed types. Can you explain why this is, or provide a reference to literature where it was investigated? I still (even after getting a PhD in compiling functional languages!) do not understand why you could not create code parameterised over the sizes of the arguments. For example, a 'cons' cell could be represented as first the size of the 'car' in bytes, then the 'car' value inline/unboxed, then a pointer to the 'cdr' cell. The Sixten language[0] does this, although it's still very early in its development. I'm not saying this is necessarily a good solution, I just wonder why I have never seen it seriously considered (and perhaps rejected). In practice, I do believe that monomorphisation is very often a good strategy. [0]: https://github.com/ollef/sixten https://github.com/ollef/sixten

gpderetta 8y ago
> why you could not create code parameterised over the sizes of the arguments If I understand correctly, that's what BitC was trying to do, but the extreme complexity of the compilation model was cited as one of the reasons the project failed. The postmortem is here I think, but I can't access it right now: http://www.coyotos.org/pipermail/bitc-dev/2012-March/003300.html http://www.coyotos.org/pipermail/bitc-dev/2012-March/003300....