Abstract
Work-efficient parallel mergesort
Author: Sam Westrick <shwestrick@gmail.com.
Synopsis
val merge_sort_with_params | [n] 't : | {max_block_size: i64, max_merge_block_size: i64} -> (leq: t -> t -> bool) -> (s: [n]t) -> [n]t |
val merge_sort | [n] 't : | (leq: t -> t -> bool) -> (s: [n]t) -> [n]t |
val merge_sort_by_key | [n] 't 'k : | (key: t -> k) -> (leq: k -> k -> bool) -> (s: [n]t) -> [n]t |
val merge_sort_with_params_by_key | [n] 't 'k 't₂₄ : | (params: {max_block_size: i64, max_merge_block_size: i64}) -> (key: t -> t₂₄) -> (leq: t₂₄ -> t₂₄ -> bool) -> (s: [n]t) -> [n]t |
Description
- ↑val merge_sort_with_params [n] 't: {max_block_size: i64, max_merge_block_size: i64} -> (leq: t -> t -> bool) -> (s: [n]t) -> [n]t
Work-efficient parallel mergesort:
merge_sort_with_params {max_block_size, max_merge_block_size} leq s
Any values for {max_block_size, max_merge_block_size} are acceptable, but do heavily impact performance. See
merge_sort
below for reasonable choices that seem to work well in practice.- ↑val merge_sort [n] 't: (leq: t -> t -> bool) -> (s: [n]t) -> [n]t
- ↑val merge_sort_by_key [n] 't 'k: (key: t -> k) -> (leq: k -> k -> bool) -> (s: [n]t) -> [n]t
- ↑val merge_sort_with_params_by_key [n] 't 'k 't₂₄: (params: {max_block_size: i64, max_merge_block_size: i64}) -> (key: t -> t₂₄) -> (leq: t₂₄ -> t₂₄ -> bool) -> (s: [n]t) -> [n]t