7 ms·

Typelevel quicksort in Scala

60 points by lelf 11y ago

ajkjk 11y ago
[warning: ignorant musing of someone who doesn't know Scala below] This makes me wonder if 'values' can be though of as just subtypes of their types. '5' extends 'Number', say. Is this how it's interpreted in the fully-functional paradigm? If you have def fn(x: Int) : Int then 'Int' is the type of all Ints, and you have to provide a specific int - which is a subtype of Int, but you could imagine there being a subtype between 'Int' and '5', like: 5 <: intermediateType <: Int So in order to 'invoke' a function you have to provide a subtype that reduces it to one value, at the level of 5, not just any subtype of int. Meaning that something about '5' makes it a special kind of subtype that can actually be used to execute the function. Maybe that's what we mean by 'value'. I don't know. I do find the idea that fn(5) is a subtype of fn(x: Int) to be cute. And that def foo(x: Int): Int = fn(x) has the 'subtype' foo(5): fn(5) seems suggestive.
- kryptiskt 11y ago
  You may be interested in how Typed Racket does types. http://docs.racket-lang.org/ts-reference/type-ref.html http://docs.racket-lang.org/ts-reference/type-ref.html
- CHY872 11y ago
  For a bit of theoretical background, try http://www.cl.cam.ac.uk/teaching/1415/Types/types.notes.pdf http://www.cl.cam.ac.uk/teaching/1415/Types/types.notes.pdf (it's fairly easy reading). I'm not sure I quite understand what you're saying completely, but typically we distinguish types from values because we otherwise find it very difficult to write a performant typing algorithm. Personally, I try to avoid subtyping where possible; I usually end up getting weird contradictions.
- tel 11y ago
  There's some significant sense to what you're talking about, so I'll share some pointers into deeper waters. The idea of a value being a type is the nature of "dependently typed" languages. However, they do it the other way around: types are merely values. This is very similar to what you're saying except DT languages would not have that 5 : 5 Instead, we introduce the idea of a singleton type. It works like this: for any type A and any value (x : A), we have a type (Sing A x) with exactly one value, (TheSing x : Sing A x). The other thing to keep in mind is that subtyping is kind of a rocky place to lay your type semantics. This is rough because most people are used to subtyping in their types. Instead, we note that whenever we have that (A :> B) then we have a function (A -> B) which is injective (really, an "epimorphism"). This broaden's our view to consider any injective function between types instead of merely some subtyping relation. Immediately it ought to be clear that (a) this is intractable automatically and (b) it's far more rich. Then it turns out that subtyping itself is fairly intractable (which subtypes are the right ones? there are many types intermediate between (Sing Integer 5) and (Integer)). So throw away automatic subsumption and require explicit coercions. This is workable and indeed in use today.
  - ajkjk 11y ago
    This is really interesting, thanks.
  - seanmcdirmid 11y ago
    It seems that you can either fight subtyping (by avoiding it) or embrace it; e.g. with pure subtype system: http://people.tamu.edu/~hiraditya/index_files/ProgLang_Presentation.pdf http://people.tamu.edu/~hiraditya/index_files/ProgLang_Prese... You do exchange a typing judgment for a subtyping one. I feel like we haven't really looked at subtyping enough. It might not be so hard as it is different, that our existing type systems simply aren't suited to it but we could come up with subtype systems that are.
steven2012 11y ago
What sort of support does Scala have going forward? My understanding is that although there are a lot of scala users, a lot of major corporate users have backed away from it, ex. LinkedIn, Twitter, etc, because of fundamental issues with the language.
- pkinsky 11y ago
  I keep hearing this, but the fact is that both companies continue to use Scala for core functions. There are plenty of Scala jobs out there.
- salex89 11y ago
  Never heard of Twitter abandoning Scala. They actually seem committed. LinkedIn changes technology often. But that does not have to mean much. It is still well used and on surveys immediately after the regulars such as java, python, c++,c#, js.
- gclaramunt 11y ago
  Dunno, I know plenty of major corporate users that are adopting Scala, I bet I can name two adopters for each one you know that backed away from it... And not "we use it in this dark corner where nobody cares", more like "is the backbone of our new business"
- lmm 11y ago
  As someone who's recently been jobhunting, Scala feels more popular than ever. It may no longer be as hyped as it was (which is probably better for everyone), but it's still growing. And really there is no alternative - once you've used higher-kinded types there's no going back. Some organizations make the switch to Haskell, but that's not an option in many environments. Other than that, if you want higher-kinded types there's nothing that's remotely as mature as Scala out there. I can't speak to "fundamental issues with the language" because I haven't found any.
  - seanmcdirmid 11y ago
    > And really there is no alternative - once you've used higher-kinded types there's no going back. Do companies that have adopted Scala really value higher-kinded typing that much?
faldore 11y ago
Is there a practical application? Are there any benefits to using the type system for quicksorting?
brudgers 11y ago
This is cool and clever. But if it doesn't sort in O(1) memory, it's not quicksort. With the lambda calculus lacking a concept of place, it's always going to be tough ensure sorting in place...or randomized pivots as in Hoare's algorithm.
- sjolsen 11y ago
  Quicksort is O(log n) space, not O(1).
  - nightcracker 11y ago
    And if you're implementing pure Quicksort you have to make sure to recurse on the smaller partition first, otherwise you're using O(n) space in the worst case. You don't have to do this if you're already using a hybrid sort to prevent Quicksort's worst case, like introsort or (shameless self promotion) pdqsort (https://github.com/orlp/pdqsort https://github.com/orlp/pdqsort).
    - sjolsen 11y ago
      >you have to make sure to recurse on the smaller partition first, otherwise you're using O(n) space in the worst case I haven't run the math, but I don't believe introsort fixes this. It's a constant-factor optimization.
      - nightcracker 11y ago
        Introsort switches to heapsort if the recursion depth becomes too big to limit runtime to O(n log n), which indirectly also limits space to O(log n).

60 points by lelf 11y ago

ajkjk 11y ago

[warning: ignorant musing of someone who doesn't know Scala below] This makes me wonder if 'values' can be though of as just subtypes of their types. '5' extends 'Number', say. Is this how it's interpreted in the fully-functional paradigm? If you have def fn(x: Int) : Int then 'Int' is the type of all Ints, and you have to provide a specific int - which is a subtype of Int, but you could imagine there being a subtype between 'Int' and '5', like: 5 <: intermediateType <: Int So in order to 'invoke' a function you have to provide a subtype that reduces it to one value, at the level of 5, not just any subtype of int. Meaning that something about '5' makes it a special kind of subtype that can actually be used to execute the function. Maybe that's what we mean by 'value'. I don't know. I do find the idea that fn(5) is a subtype of fn(x: Int) to be cute. And that def foo(x: Int): Int = fn(x) has the 'subtype' foo(5): fn(5) seems suggestive.

kryptiskt 11y ago
You may be interested in how Typed Racket does types. http://docs.racket-lang.org/ts-reference/type-ref.html http://docs.racket-lang.org/ts-reference/type-ref.html
CHY872 11y ago
For a bit of theoretical background, try http://www.cl.cam.ac.uk/teaching/1415/Types/types.notes.pdf http://www.cl.cam.ac.uk/teaching/1415/Types/types.notes.pdf (it's fairly easy reading). I'm not sure I quite understand what you're saying completely, but typically we distinguish types from values because we otherwise find it very difficult to write a performant typing algorithm. Personally, I try to avoid subtyping where possible; I usually end up getting weird contradictions.
tel 11y ago
There's some significant sense to what you're talking about, so I'll share some pointers into deeper waters. The idea of a value being a type is the nature of "dependently typed" languages. However, they do it the other way around: types are merely values. This is very similar to what you're saying except DT languages would not have that 5 : 5 Instead, we introduce the idea of a singleton type. It works like this: for any type A and any value (x : A), we have a type (Sing A x) with exactly one value, (TheSing x : Sing A x). The other thing to keep in mind is that subtyping is kind of a rocky place to lay your type semantics. This is rough because most people are used to subtyping in their types. Instead, we note that whenever we have that (A :> B) then we have a function (A -> B) which is injective (really, an "epimorphism"). This broaden's our view to consider any injective function between types instead of merely some subtyping relation. Immediately it ought to be clear that (a) this is intractable automatically and (b) it's far more rich. Then it turns out that subtyping itself is fairly intractable (which subtypes are the right ones? there are many types intermediate between (Sing Integer 5) and (Integer)). So throw away automatic subsumption and require explicit coercions. This is workable and indeed in use today.
- ajkjk 11y ago
  This is really interesting, thanks.
- seanmcdirmid 11y ago
  It seems that you can either fight subtyping (by avoiding it) or embrace it; e.g. with pure subtype system: http://people.tamu.edu/~hiraditya/index_files/ProgLang_Presentation.pdf http://people.tamu.edu/~hiraditya/index_files/ProgLang_Prese... You do exchange a typing judgment for a subtyping one. I feel like we haven't really looked at subtyping enough. It might not be so hard as it is different, that our existing type systems simply aren't suited to it but we could come up with subtype systems that are.

steven2012 11y ago

What sort of support does Scala have going forward? My understanding is that although there are a lot of scala users, a lot of major corporate users have backed away from it, ex. LinkedIn, Twitter, etc, because of fundamental issues with the language.

pkinsky 11y ago
I keep hearing this, but the fact is that both companies continue to use Scala for core functions. There are plenty of Scala jobs out there.
salex89 11y ago
Never heard of Twitter abandoning Scala. They actually seem committed. LinkedIn changes technology often. But that does not have to mean much. It is still well used and on surveys immediately after the regulars such as java, python, c++,c#, js.
gclaramunt 11y ago
Dunno, I know plenty of major corporate users that are adopting Scala, I bet I can name two adopters for each one you know that backed away from it... And not "we use it in this dark corner where nobody cares", more like "is the backbone of our new business"
lmm 11y ago
As someone who's recently been jobhunting, Scala feels more popular than ever. It may no longer be as hyped as it was (which is probably better for everyone), but it's still growing. And really there is no alternative - once you've used higher-kinded types there's no going back. Some organizations make the switch to Haskell, but that's not an option in many environments. Other than that, if you want higher-kinded types there's nothing that's remotely as mature as Scala out there. I can't speak to "fundamental issues with the language" because I haven't found any.
- seanmcdirmid 11y ago
  > And really there is no alternative - once you've used higher-kinded types there's no going back. Do companies that have adopted Scala really value higher-kinded typing that much?

faldore 11y ago

Is there a practical application? Are there any benefits to using the type system for quicksorting?

brudgers 11y ago

This is cool and clever. But if it doesn't sort in O(1) memory, it's not quicksort. With the lambda calculus lacking a concept of place, it's always going to be tough ensure sorting in place...or randomized pivots as in Hoare's algorithm.

sjolsen 11y ago
Quicksort is O(log n) space, not O(1).
- nightcracker 11y ago
  And if you're implementing pure Quicksort you have to make sure to recurse on the smaller partition first, otherwise you're using O(n) space in the worst case. You don't have to do this if you're already using a hybrid sort to prevent Quicksort's worst case, like introsort or (shameless self promotion) pdqsort (https://github.com/orlp/pdqsort https://github.com/orlp/pdqsort).
  - sjolsen 11y ago
    >you have to make sure to recurse on the smaller partition first, otherwise you're using O(n) space in the worst case I haven't run the math, but I don't believe introsort fixes this. It's a constant-factor optimization.
    - nightcracker 11y ago
      Introsort switches to heapsort if the recursion depth becomes too big to limit runtime to O(n log n), which indirectly also limits space to O(log n).