From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: Received: from mail3-relais-sop.national.inria.fr (mail3-relais-sop.national.inria.fr [192.134.164.104]) by sympa.inria.fr (Postfix) with ESMTPS id 6574FE000E for ; Thu, 20 Aug 2020 15:37:51 +0200 (CEST) Authentication-Results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=oleg@okmij.org; spf=Pass smtp.mailfrom=oleg@okmij.org; spf=None smtp.helo=postmaster@mail1.g3.pair.com Received-SPF: None (mail3-smtp-sop.national.inria.fr: no sender authenticity information available from domain of oleg@okmij.org) identity=pra; client-ip=66.39.3.114; receiver=mail3-smtp-sop.national.inria.fr; envelope-from="oleg@okmij.org"; x-sender="oleg@okmij.org"; x-conformance=sidf_compatible Received-SPF: Pass (mail3-smtp-sop.national.inria.fr: domain of oleg@okmij.org designates 66.39.3.114 as permitted sender) identity=mailfrom; client-ip=66.39.3.114; receiver=mail3-smtp-sop.national.inria.fr; envelope-from="oleg@okmij.org"; x-sender="oleg@okmij.org"; x-conformance=sidf_compatible; x-record-type="v=spf1" Received-SPF: None (mail3-smtp-sop.national.inria.fr: no sender authenticity information available from domain of postmaster@mail1.g3.pair.com) identity=helo; client-ip=66.39.3.114; receiver=mail3-smtp-sop.national.inria.fr; envelope-from="oleg@okmij.org"; x-sender="postmaster@mail1.g3.pair.com"; x-conformance=sidf_compatible IronPort-PHdr: =?us-ascii?q?9a23=3AMUXCOh01Hq0fgVPMsmDT+DRfVm0co7zxezQtwd8Z?= =?us-ascii?q?se0eLPad9pjvdHbS+e9qxAeQG9mCtbQd0rKd7/2ocFdDyK7JiGoFfp1IWk1Nou?= =?us-ascii?q?QttCtkPvS4D1bmJuXhdS0wEZcKflZk+3amLRodQ56mNBXdrXKo8DEdBAj0OxZr?= =?us-ascii?q?KeTpAI7SiNm82/yv95HJbAhEmTuwbalvIBmrsQnducYbjIt/Iast1xXFpWdFdf?= =?us-ascii?q?5Lzm1yP1KTmBj85sa0/JF99ilbpuws+c1dX6jkZqo0VbNXAigoPGAz/83rqALM?= =?us-ascii?q?TRCT6XsGU2UZiQRHDg7Y5xznRJjxsy/6tu1g2CmGOMD9UL45VSi+46ptVRTljj?= =?us-ascii?q?oMOTwk/2HNksF+gqJVrgy8qRJ8zIHbfJyaO/Rlc6PBYd8XX3ZNUtpLWiBfBI63?= =?us-ascii?q?cosBD/AGPeZdt4Tzvl8OogWxBQKxA+7vzTtIiWH53aAh1OQhEgTG3A0iH94Ut3?= =?us-ascii?q?TUttr1Ob4UXOuow6bG0S/NYOlK2Tfh9ofIaBYhrOmPULx+f8fcy1ciGgzbg1ie?= =?us-ascii?q?rYHpIy+Z2OsPvmaV4edtWuCihm07pg9xvjWiydkhhpTGiI4Lyl7I6yp3zYI1K9?= =?us-ascii?q?O2TkNwfNCqEJxVty6ANot2RNsvQ2ZruCY/y70Gu4S3fC8QyJQowRPUdv+Jc5CQ?= =?us-ascii?q?7x/iVeudOzl1iXZ/dL+xnRq+7FWsx+LkWsWp0VtHoDBJn9bIu3wXyRDf98aKRu?= =?us-ascii?q?F/80u93zuEyhrd5fteIU8ukKrWM54hzaA0lpoUqUnDGzX5mETyjKOLbEkk9eal?= =?us-ascii?q?5/7/Yrr8p5+cLZV4hR35MqQrgsC/AOI4PRYSX2WD+Omx1afv8EP9TblQgPA6iL?= =?us-ascii?q?TVvI3VKMgDo662GQ5V0oIt6xalCDem1cwVnX4DLF1bdxKKlI/pO1LLIPD5D/ez?= =?us-ascii?q?mVOskC1kx/zeJL3uHo3NLmTfkLfmZbty91RTyA83zdxG45JUC6oBIO7oV0/qtN?= =?us-ascii?q?3YCwc5PBauz+bmDtV9zIIeVniVDq+XKqOB+WOPs+kmJu3JYI4OpB78LeIk7rjg?= =?us-ascii?q?lywXg1gYKI6t0JRfPHe8E/tOJEacYHiqhc0ORzRZ9jEiRfDn3QXRGQVYYGy/Cv?= =?us-ascii?q?plt2MLTbm+BIKGfbiDxbmI3SO1BJpTPzkUDVOJEHWucJ+LCa5VNXCiZ/R5mzlB?= =?us-ascii?q?boCPDo8s0Rb35V3/wrtjd6zboWsAvJP5ktNy4r+LzE1gxXlPF82Yllq1YSRshG?= =?us-ascii?q?pRHm0x36V+owp60FjRiaU=3D?= X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: =?us-ascii?q?A0A6AgDNez5fmHIDJ0JfgQmBTIMYVQExL?= =?us-ascii?q?I04pEQLAQMBDCMKAgQBAYcQAhwHAQQ0EwIQAQEFAQEBAgEDAwQBEwEBAQEBCAs?= =?us-ascii?q?LBimFYwxDARABgWIig1mBNIQCAYJ7AQ+xSYE0iwSBOAGNHw4NgUBAg3ODMQwLB?= =?us-ascii?q?IIqgn2CLQSbdpoVLoJtgRmBKYYikS8wgwGBI4EdmmgBhVmIH4Y1iFqVJYFrgXp?= =?us-ascii?q?NMAg7gmoIRxkNjjmIa4VRMgEyNwIGCgEBAwlYhD+MNgEB?= X-IPAS-Result: =?us-ascii?q?A0A6AgDNez5fmHIDJ0JfgQmBTIMYVQExLI04pEQLAQMBDCM?= =?us-ascii?q?KAgQBAYcQAhwHAQQ0EwIQAQEFAQEBAgEDAwQBEwEBAQEBCAsLBimFYwxDARABg?= =?us-ascii?q?WIig1mBNIQCAYJ7AQ+xSYE0iwSBOAGNHw4NgUBAg3ODMQwLBIIqgn2CLQSbdpo?= =?us-ascii?q?VLoJtgRmBKYYikS8wgwGBI4EdmmgBhVmIH4Y1iFqVJYFrgXpNMAg7gmoIRxkNj?= =?us-ascii?q?jmIa4VRMgEyNwIGCgEBAwlYhD+MNgEB?= X-IronPort-AV: E=Sophos;i="5.76,332,1592863200"; d="scan'208";a="356921573" X-MGA-submission: =?us-ascii?q?MDEe9pPVJEgZmeuKDB9Go6VHGhgugZheGCC+g+?= =?us-ascii?q?zYX0vQZhcxAgiqANyJNT2kPteb7cdSxlPPiP+jMfxXbVVe6tUx5QsLDF?= =?us-ascii?q?A5Jd4clvqxHwrNaUzo1TFiP6URcOCFHdlGZQzsryjtDHCj44RmhMAdOu?= =?us-ascii?q?Mwbdpze/YUPzBwt9sleIXjvw=3D=3D?= Received: from mail1.g3.pair.com ([66.39.3.114]) by mail3-smtp-sop.national.inria.fr with ESMTP/TLS/DHE-RSA-AES256-GCM-SHA384; 20 Aug 2020 15:37:49 +0200 Received: from mail1.g3.pair.com (localhost [127.0.0.1]) by mail1.g3.pair.com (Postfix) with ESMTP id E9FBA3FBA60; Thu, 20 Aug 2020 09:37:46 -0400 (EDT) Received: from Melchior.localnet (70.213.49.163.rev.vmobile.jp [163.49.213.70]) (using TLSv1.2 with cipher ECDHE-RSA-AES256-GCM-SHA384 (256/256 bits)) (No client certificate requested) by mail1.g3.pair.com (Postfix) with ESMTPSA id 23FD058359C; Thu, 20 Aug 2020 09:37:45 -0400 (EDT) Date: Thu, 20 Aug 2020 22:41:51 +0900 From: Oleg To: caml-list@inria.fr Message-ID: <20200820134151.GA4611@Melchior.localnet> Mail-Followup-To: Oleg , caml-list@inria.fr MIME-Version: 1.0 Content-Type: text/plain; charset=us-ascii Content-Disposition: inline User-Agent: Mutt/1.10.1 (2018-07-13) Subject: [Caml-list] (ANN) Lightweight HList -- typed heterogeneous collections This is a (very late) announcement of the pure OCaml lightweight analogue of HList -- typed heterogeneous collections. Such collections store data of various types, and offer element access/modification plus bulk operations such as mapping and iteration. In HList, the type of the collection reflects the types of the elements; therefore all type mismatches can be detected statically. Correspondingly, there is no need to store any type information at run-time. The library was actually written two years ago. I have just realized I neglected to announce it. The implementation is fairly trivial, but does come useful from time to time, e.g., to implement polyvariadic functions. One interesting facility is the ability to replace an element somewhere in a collection with a new one of a different type. The type of the returned collection is changed accordingly. A more detailed description, and the pointer to the code is: http://okmij.org/ftp/ML/ML.html#hlist The code contains several examples, including multi-dimensional cartesian product: converting an HList of regular lists to a list of tuples, elements of the cartesian product. A somewhat non-trivial application of HList (specifically, type-changing update) is the tagless-final embedding of simply-typed lambda-calculus with De Bruijn *levels*: http://okmij.org/ftp/tagless-final/cookbook.html#dblevels At first glance, an embedding that relies on OCaml typechecker to check and infer types of lambda-terms seems impossible.