[Caml-list] [ANN] ilist-0.1.0 - indexed lists

[Caml-list] [ANN] ilist-0.1.0 - indexed lists

[Wojciech Meyer]

Hi,

I'm happy to release a small library that brings up to use convenience
and safety of indexed lists using GADT encodings.

The tarball can be fetched here:

http://danmey.org/ilist-0.1.0.tar.gz

OPAM packaging will be available shortly.

Currently the library contains just two modules:

NList - length indexed list
IList - heterogeneous list where each element can have it's own type

syntax extension:

Pa_ilist - allows to use the list literals and pattern matching on the
           lists. While using Camlp4 might be useful, it's being
           considered to use -ppx extensions instead present on the
           current OCaml trunk.

and plenty of examples what can be done using the library.

NList can be used everywhere we need an invariant on length encoded in a
type. For instance now a list of at least one element encoded as a tuple
of the first element and the rest as a list now can be encoded directly
as an Nlist.

IList is probably most similar to tuples with one exception, that now we
can encode a generic extraction and extending functions that will work
on any sized lists (compare IList.hd to fst), so it behaves like an
extensible tuple.

Project home:     https://github.com/danmey/Ilist
Bugs & features:  https://github.com/danmey/Ilist/issues
License:          BSD3

Thanks,
--
Wojciech Meyer
http://danmey.org

Re: [Caml-list] [ANN] ilist-0.1.0 - indexed lists

[Erkki Seppala]

Wojciech Meyer <wojciech.meyer@gmail.com> writes:

> Hi,
>
> I'm happy to release a small library that brings up to use convenience
> and safety of indexed lists using GADT encodings.

Pretty nice! But I must not be the only one thinking this would be even
more useful with arrays? I imagine it would need to be a bit different,
have the array type alongside with similar kind of linked list of types.

Do you think it would be doable, though?

-- 
  _____________________________________________________________________
     / __// /__ ____  __               http://www.modeemi.fi/~flux/\   \
    / /_ / // // /\ \/ /                                            \  /
   /_/  /_/ \___/ /_/\_\@modeemi.fi                                  \/

Re: [Caml-list] [ANN] ilist-0.1.0 - indexed lists

[Wojciech Meyer]

Erkki Seppala <flux-caml@inside.org> writes:

> Pretty nice! But I must not be the only one thinking this would be even
> more useful with arrays? I imagine it would need to be a bit different,
> have the array type alongside with similar kind of linked list of
> types.
Thanks.
>
> Do you think it would be doable, though?

I can't see it. I believe it would be only practical with a decent
syntax extension. We would need be able to encode the length inside the
type, and for arrays this might be quite huge - however this would be no
problem part (apart from efficiency of type checking), the problematic
part would be to encode the concatenation of arrays - which can be done
as in omega encoding using witnesses. Also then random access of arrays
would need sort of natural encoded integers. One could even think about
arrays of size n^2 supporting only doubling the size.

We would be getting here to dependent types, that's probably why I
decided that Ilist is would not be a collection of data structures.

--
Wojciech Meyer
http://danmey.org