The fundamental problem with GADT is that it leads to a “closed”
implementation:
Only the library implementor can handle new cases; the users cannot.
I tried a bit. Using templates to implement the dsort function seems rather
involved.
Here is a sketch based on GADT:
extern
fun
{x:vt@ype}
bsortChar{n:int}
(list_vt((char, x), n)): list_vt((char, x), n)
extern
fun
{x:vt@ype}
bsortNat{n:int}
(intGte(0), list_vt((int, x), n)): list_vt((int, x), n)
datatype
Order(t@ype) =
| Char(char)
| Nat(int) of intGte(0)
| {k1,k2:t@ype}
Pair((k1, k2)) of (Order(k1), Order(k2))
extern
fun
{k:t@ype}
{x:vt@ype}
dsort{n:int}
(ord: Order(k), kxs: list_vt((k, x), n)): list_vt((k, x), n)
extern
fun{
x:vt0p}{y:vt0p
} list_vt_mapfree_fun{n:int}
(list_vt (INV(x), n), f: (&x >> x?) → y): list_vt (y, n)
implement
{k}{x}
dsort (ord, kxs) =
(
case+ ord of
| Char() => bsortChar(kxs)
| Nat(bound) => bsortNat(bound, kxs)
| Pair{k1,k2}(ord1, ord2) => kxs where
{
val k2kxs =
list_vt_mapfree_fun<(k,x)><(k2,@(k,x))> (kxs, lam kx => ((kx.0).1, kx
))
val k2kxs = dsort(ord2, k2kxs)
val kxs = list_vt_mapfree_fun<(k2,@(k,x))><(k,x)> (k2kxs, lam k2kx =>
k2kx.1)
val k1kxs =
list_vt_mapfree_fun<(k,x)><(k1,@(k,x))> (kxs, lam kx => ((kx.0).0, kx
))
val k1kxs = dsort(ord1, k1kxs)
val kxs = list_vt_mapfree_fun<(k1,@(k,x))><(k,x)> (k1kxs, lam k2kx =>
k2kx.1)
}
)
A very big factor in the efficiency of an implementation of a sorting
algorithm is whether it can handle flat data.
This issue is not mentioned at all in the paper.On Wednesday, February 18, 2015 at 1:45:33 AM UTC-5, H Zhang wrote:
The GHC user guide credit you as a pioneer of GADT/GRDT
http://www.cs.bu.edu/~hwxi/academic/papers/popl03.pdf: “These and many
other examples are given in papers by Hongwei Xi, and Tim Sheard.”
https://downloads.haskell.org/~ghc/6.6.1/docs/html/users_guide/gadt.html
I find the GADT as implemented in Haskell pretty easy to follow. Do you no
longer think it is a good way for generic programming? Can you sketch out
how ATS template programming would express similar ideas (e.g. from the
discriminator paper)? In ATS can one do pattern matching on template type
parameters? If not how does one structurally decompose the type parameters?
Sorry for my naivete on this matter.
On Tuesday, February 17, 2015 at 4:44:00 PM UTC-8, gmhwxi wrote:
I was not familiar with generic discrimination.
I took a quick look at the paper last night. I feel it should be
straightforward to implement
the algorithm in ATS. Actually, it seems only natural to use a linear
type for values (not keys)
in such an implementation. I would not use GADT (or GRDT as I call it); I
would use templates
instead.
On Monday, February 16, 2015 at 11:33:38 PM UTC-5, H Zhang wrote:
Prof. Xi,
I am not sure if you are familiar with Fritz Henglein’s work on Generic
discrimination: Sorting and partitioning unshared data in linear time
http://www.diku.dk/hjemmesider/ansatte/henglein/papers/henglein2008.pdf?
Now before people ask how is linear time sorting possible, no it is not if
you define the comparison arbitrarily. However most interesting sorts are
on recursively defined orders that reduce to the lexicographic order of
primitive types in which case bucket sort is linear time (by taking
advantage of the constant access time of the RAM). In his work Henglein
showed how to generically perform this type of sorting using GADT in
Haskell. This would be an ideal application of ATS if it is doable. Indeed
as the author pointed out in conclusion:
“The present functional specification of discrimination has been
formulated for clarity, and—most emphatically—not for performance beyond
enabling some basic asymptotic reasoning. Even though it appears to perform
competitively out-of-the-box with good sorting algorithms in terms of time
performance, it appears clear that its memory requirements need to—and
can—be managed explicitly in a practical implementation. In particular,
efficient in-place implementations that do away with the need for dynamic
memory management, reduce the memory footprint and improve data locality
should provide substantial benefits in comparison to leaving memory
management to a general-purpose heap manager.”
So could ATS’s linear types and generic programming facilities could be
used to make this practical?
Haitao
http://www.diku.dk/hjemmesider/ansatte/henglein/papers/henglein2008.pdf