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 mail2-relais-roc.national.inria.fr (mail2-relais-roc.national.inria.fr [192.134.164.83]) by sympa.inria.fr (Postfix) with ESMTPS id 889BC7EC6E for ; Fri, 13 Jun 2014 14:10:33 +0200 (CEST) Received-SPF: None (mail2-smtp-roc.national.inria.fr: no sender authenticity information available from domain of nicolas.boulay@gmail.com) identity=pra; client-ip=209.85.213.174; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="nicolas.boulay@gmail.com"; x-sender="nicolas.boulay@gmail.com"; x-conformance=sidf_compatible Received-SPF: Pass (mail2-smtp-roc.national.inria.fr: domain of nicolas.boulay@gmail.com designates 209.85.213.174 as permitted sender) identity=mailfrom; client-ip=209.85.213.174; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="nicolas.boulay@gmail.com"; x-sender="nicolas.boulay@gmail.com"; x-conformance=sidf_compatible; x-record-type="v=spf1" Received-SPF: None (mail2-smtp-roc.national.inria.fr: no sender authenticity information available from domain of postmaster@mail-ig0-f174.google.com) identity=helo; client-ip=209.85.213.174; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="nicolas.boulay@gmail.com"; x-sender="postmaster@mail-ig0-f174.google.com"; x-conformance=sidf_compatible X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: AjABALbpmlPRVdWulWdsb2JhbABag19ZgmzAGXwIFg8BAQEBBw0JCRIqhAMBAQEDARIRHQExBwEDAQsBBQUEBw0qAgIiEgEFARwGEyKIDAMJCA2mSmqLJ4UBk3gnDYYGEQEBBAyOTIMAgUwEmjaRYxgpgWmDBTs X-IPAS-Result: AjABALbpmlPRVdWulWdsb2JhbABag19ZgmzAGXwIFg8BAQEBBw0JCRIqhAMBAQEDARIRHQExBwEDAQsBBQUEBw0qAgIiEgEFARwGEyKIDAMJCA2mSmqLJ4UBk3gnDYYGEQEBBAyOTIMAgUwEmjaRYxgpgWmDBTs X-IronPort-AV: E=Sophos;i="5.01,471,1400018400"; d="scan'208";a="79894963" Received: from mail-ig0-f174.google.com ([209.85.213.174]) by mail2-smtp-roc.national.inria.fr with ESMTP/TLS/RC4-SHA; 13 Jun 2014 14:10:12 +0200 Received: by mail-ig0-f174.google.com with SMTP id h3so439678igd.13 for ; Fri, 13 Jun 2014 05:10:10 -0700 (PDT) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20120113; h=mime-version:sender:in-reply-to:references:date:message-id:subject :from:to:cc:content-type; bh=EaYyPuyfLUPTY/K5hoFuNI84d1vI8UQ/yVaAESlkUzs=; b=r4NYjOB62goUWkz0D7rNUUed3E/HhW+Z/mZErlS2iYd+FMERGekqqc3CCuPExR/bmr RpRZAa1BWuiHxjSLTNK7fnAL+Rf+McZg/xN7+DVWlWYyuUSkV/3pIbTYa50w/LDiYjmA IbwJbzEScWK2ciVU4QvsxyNeTy0Nieucy3XgS3ulFnrlsUeteJe90LhnbXE19hUhrcPF hKJsfwBjxLWDYjI1RyM6LYS5tLmcHWjV7EoPL/C8TOzB14lXBFW6MMu+JVAKdPY8N5Kx lfPxJvudk+V83qIZpWykGblGBVnb56y8cLU92pGC8fyKpXUFK/lrABv71wv2DDz32Nq+ OxSg== MIME-Version: 1.0 X-Received: by 10.43.53.73 with SMTP id vp9mr2663841icb.61.1402661410798; Fri, 13 Jun 2014 05:10:10 -0700 (PDT) Sender: nicolas.boulay@gmail.com Received: by 10.50.50.135 with HTTP; Fri, 13 Jun 2014 05:10:10 -0700 (PDT) In-Reply-To: <20140613095403.GB18282@traveler> References: <20140613095403.GB18282@traveler> Date: Fri, 13 Jun 2014 14:10:10 +0200 X-Google-Sender-Auth: gigDNNDuycFIpJhG25zAeb7LE0Y Message-ID: From: Nicolas Boulay To: Roberto Di Cosmo Cc: caml users Content-Type: multipart/alternative; boundary=bcaec5299be32180f204fbb68fc8 X-Validation-by: nicolas@boulay.name Subject: Re: [Caml-list] Adding Dimensions to types --bcaec5299be32180f204fbb68fc8 Content-Type: text/plain; charset=UTF-8 2014-06-13 11:54 GMT+02:00 Roberto Di Cosmo : > On Fri, Jun 13, 2014 at 11:43:20AM +0200, Gabriel Scherer wrote: > > Encoding integers with addition at the type level is easy enough (it > > is possible to use a technique akin to difference list where you keep > > unary numbers with a unification variable at their tail, to get the > > unification engine to do the addition for you). Anything below that, > > in particular substraction, cannot be done *conveniently* in the > > type-system. It is possible to encode arbitrary operation on > > type-level numbers (unary or not), expressed relationally > > (Prolog-style: ('a, 'b, 'c) add is inhabited if 'a+'b='c) by a GADT > > witnessing the relation, but actually building and using these > > operations then requires the programmer to provide those witness terms > > that are manipulated at runtime. > > Actually, we want to have dimension checking at compile time, with no > trace of it at runtime. > Is it possible to think with dimension inference ? This avoid the need to give dimension everywhere. You can have rules like if "a + b = c" => dim(a) == dim(b) == dim(c). if(e*f=g) => dim(g) = dim(e) * dim(f) You can even go further. https://en.wikipedia.org/wiki/Dimensional_analysis gives some hint : Position vs displacement. if T1 and T2 are absolut point in time, (T1-T2) are time offset. But "T1 + T2" is a none sense. You could also extend the check of dimension in space direction (x,y,z). The idea is to add a check with minimum new user input. Nicolas --bcaec5299be32180f204fbb68fc8 Content-Type: text/html; charset=UTF-8 Content-Transfer-Encoding: quoted-printable



2014-06-13 11:54 GMT+02:00 Roberto Di Cosmo <<= a href=3D"mailto:roberto@dicosmo.org" target=3D"_blank">roberto@dicosmo.org= >:
On Fri, J= un 13, 2014 at 11:43:20AM +0200, Gabriel Scherer wrote:
> Encoding integers with addition at the type level is easy enough (it > is possible to use a technique akin to difference list where you keep<= br> > unary numbers with a unification variable at their tail, to get the
> unification engine to do the addition for you). Anything below that, > in particular substraction, cannot be done *conveniently* in the
> type-system. It is possible to encode arbitrary operation on
> type-level numbers (unary or not), expressed relationally
> (Prolog-style: ('a, 'b, 'c) add is inhabited if 'a+= 9;b=3D'c) by a GADT
> witnessing the relation, but actually building and using these
> operations then requires the programmer to provide those witness terms=
> that are manipulated at runtime.

Actually, we want to have dimension checking at compile time, with no=
trace of it at runtime.

Is it possible to think with dimension inference ? This avoid the n= eed to give dimension everywhere.

You can have rules like
if "a + b =3D c" =3D> dim(a) =3D= =3D dim(b) =3D=3D dim(c).
if(e*f=3Dg) = =3D> dim(g) =3D dim(e) * dim(f)

=
You can even go further. https://en.wikipedia.org/wiki/Dimensional_analysis gives s= ome hint :=C2=A0 Position vs displacement.

if T1 and T2 are absolut point in time, (T1-T2) are time offset. But "= T1 + T2"=C2=A0 is a none sense.

You could also extend the check of dimension in space direction (x,y,z).<= br>
The idea is to add a check with minimu= m new user input.

Nicolas
--bcaec5299be32180f204fbb68fc8--