From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: X-Original-To: caml-list@sympa.inria.fr Delivered-To: caml-list@sympa.inria.fr Received: from mail1-relais-roc.national.inria.fr (mail1-relais-roc.national.inria.fr [192.134.164.82]) by sympa.inria.fr (Postfix) with ESMTPS id 4C9117F1E1 for ; Sat, 12 Jan 2013 22:16:57 +0100 (CET) Received-SPF: None (mail1-smtp-roc.national.inria.fr: no sender authenticity information available from domain of wojciech.meyer@gmail.com) identity=pra; client-ip=74.125.82.174; receiver=mail1-smtp-roc.national.inria.fr; envelope-from="wojciech.meyer@gmail.com"; x-sender="wojciech.meyer@gmail.com"; x-conformance=sidf_compatible Received-SPF: Pass (mail1-smtp-roc.national.inria.fr: domain of wojciech.meyer@gmail.com designates 74.125.82.174 as permitted sender) identity=mailfrom; client-ip=74.125.82.174; receiver=mail1-smtp-roc.national.inria.fr; envelope-from="wojciech.meyer@gmail.com"; x-sender="wojciech.meyer@gmail.com"; x-conformance=sidf_compatible; x-record-type="v=spf1" Received-SPF: None (mail1-smtp-roc.national.inria.fr: no sender authenticity information available from domain of postmaster@mail-we0-f174.google.com) identity=helo; client-ip=74.125.82.174; receiver=mail1-smtp-roc.national.inria.fr; envelope-from="wojciech.meyer@gmail.com"; x-sender="postmaster@mail-we0-f174.google.com"; x-conformance=sidf_compatible X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: ApYBAHXR8VBKfVKujWdsb2JhbABEvg4WDgEBAQEJCQsJEgYjgh4BAQQBQAEbHQEDAQsGBQsDAhElDwEEDxEBBQEiE4gGAQMJBgSZSYwzgnuEFQoZJw1ZhncBBQyRIgOWC4EcjUw/hBc X-IronPort-AV: E=Sophos;i="4.84,458,1355094000"; d="scan'208";a="189633706" Received: from mail-we0-f174.google.com ([74.125.82.174]) by mail1-smtp-roc.national.inria.fr with ESMTP/TLS/RC4-SHA; 12 Jan 2013 22:16:56 +0100 Received: by mail-we0-f174.google.com with SMTP id x10so1396801wey.33 for ; Sat, 12 Jan 2013 13:16:56 -0800 (PST) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20120113; h=x-received:from:to:cc:subject:references:date:in-reply-to :message-id:user-agent:mime-version:content-type; bh=CYYRZUQSaEPZXIh200aACE+5Hy2ZTnYvoPZQ7tLyycM=; b=Hjbry80L/mugepNLujnZEgHVyzLUkVowsh9LB2aRH5aOXySOZy1KfrchRk8TZcbKOk d9kkfJrkZWEbPIoX5uJWT2Bb+bYBQ9R7JoXQiCRXb5lGZiU3lwl8pfdH2xhvF3FvKuSA XoWbGVLeOhOrGjKbL+gcdbFlEvh/XWBHxpqSfehic8IeiJ2OkO5zxiKDtovxGUGEmjXY K1IULjr0W8qZRFsEHpsGpGNTIXp7XdjLztY7C+64hXyIp/TmaVv23KO9Len0NpeiyUdv W4/L18I8h7PExU83CanApEtOtU2t9XhrRnHBqXxG/Y3JOScSeRG4GZ46UYVJ8jl8oPzP KKvw== X-Received: by 10.180.82.41 with SMTP id f9mr5350849wiy.25.1358025416765; Sat, 12 Jan 2013 13:16:56 -0800 (PST) Received: from spec-desktop.danmey.org (cpc1-cmbg12-0-0-cust201.5-4.cable.virginmedia.com. [86.9.116.202]) by mx.google.com with ESMTPS id bw9sm5459010wib.5.2013.01.12.13.16.54 (version=TLSv1.1 cipher=RC4-SHA bits=128/128); Sat, 12 Jan 2013 13:16:55 -0800 (PST) From: Wojciech Meyer To: Erkki Seppala Cc: caml-list@yquem.inria.fr References: Date: Sat, 12 Jan 2013 21:16:57 +0000 In-Reply-To: (Erkki Seppala's message of "Sat, 12 Jan 2013 22:56:02 +0200") Message-ID: User-Agent: Gnus/5.13 (Gnus v5.13) Emacs/24.0.94 (gnu/linux) MIME-Version: 1.0 Content-Type: text/plain Subject: Re: [Caml-list] [ANN] ilist-0.1.0 - indexed lists Erkki Seppala 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