From: Wojciech Meyer <wojciech.meyer@gmail.com>
To: Erkki Seppala <flux-caml@inside.org>
Cc: caml-list@yquem.inria.fr
Subject: Re: [Caml-list] [ANN] ilist-0.1.0 - indexed lists
Date: Sat, 12 Jan 2013 21:16:57 +0000 [thread overview]
Message-ID: <wfa9se85km.fsf@gmail.com> (raw)
In-Reply-To: <m49y5fyt925.fsf@coffee.modeemi.fi> (Erkki Seppala's message of "Sat, 12 Jan 2013 22:56:02 +0200")
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
prev parent reply other threads:[~2013-01-12 21:16 UTC|newest]
Thread overview: 3+ messages / expand[flat|nested] mbox.gz Atom feed top
2013-01-12 16:34 Wojciech Meyer
2013-01-12 20:56 ` Erkki Seppala
2013-01-12 21:16 ` Wojciech Meyer [this message]
Reply instructions:
You may reply publicly to this message via plain-text email
using any one of the following methods:
* Save the following mbox file, import it into your mail client,
and reply-to-all from there: mbox
Avoid top-posting and favor interleaved quoting:
https://en.wikipedia.org/wiki/Posting_style#Interleaved_style
* Reply using the --to, --cc, and --in-reply-to
switches of git-send-email(1):
git send-email \
--in-reply-to=wfa9se85km.fsf@gmail.com \
--to=wojciech.meyer@gmail.com \
--cc=caml-list@yquem.inria.fr \
--cc=flux-caml@inside.org \
/path/to/YOUR_REPLY
https://kernel.org/pub/software/scm/git/docs/git-send-email.html
* If your mail client supports setting the In-Reply-To header
via mailto: links, try the mailto: link
Be sure your reply has a Subject: header at the top and a blank line
before the message body.
This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox;
as well as URLs for NNTP newsgroup(s).