From mboxrd@z Thu Jan 1 00:00:00 1970 Received: (from majordomo@localhost) by pauillac.inria.fr (8.7.6/8.7.3) id KAA07788; Thu, 25 Apr 2002 10:56:23 +0200 (MET DST) X-Authentication-Warning: pauillac.inria.fr: majordomo set sender to owner-caml-list@pauillac.inria.fr using -f Received: (from weis@localhost) by pauillac.inria.fr (8.7.6/8.7.3) id KAA07863 for caml-list@pauillac.inria.fr; Thu, 25 Apr 2002 10:56:22 +0200 (MET DST) Received: from nez-perce.inria.fr (nez-perce.inria.fr [192.93.2.78]) by pauillac.inria.fr (8.7.6/8.7.3) with ESMTP id XAA32322 for ; Wed, 24 Apr 2002 23:44:41 +0200 (MET DST) Received: from isis.lip6.fr (isis.lip6.fr [132.227.60.2]) by nez-perce.inria.fr (8.11.1/8.11.1) with ESMTP id g3OLie123651 for ; Wed, 24 Apr 2002 23:44:40 +0200 (MET DST) Received: from poleia.lip6.fr (poleia.lip6.fr [132.227.201.28]) by isis.lip6.fr (8.12.2/jtpda-5.4+victor) with ESMTP id g3OLieqL013598 for ; Wed, 24 Apr 2002 23:44:40 +0200 X-pt: isis.lip6.fr Received: from singha (mail@singha.lip6.fr [132.227.204.18]) by poleia.lip6.fr (8.8.6/jtpda-5.2) with ESMTP id XAA17015 for ; Wed, 24 Apr 2002 23:44:39 +0200 (MET DST) Received: from gauthier (helo=localhost) by singha with local-esmtp (Exim 3.35 #1 (Debian)) id 170UZ5-0007jy-00 for ; Wed, 24 Apr 2002 23:44:39 +0200 Date: Wed, 24 Apr 2002 23:44:39 +0200 (CEST) From: Nadji.Gauthier@lip6.fr X-Sender: gauthier@singha.lip6.fr To: caml-list@inria.fr Subject: [Caml-list] Polymorphic Variants and Number Parameterized Types Message-ID: MIME-Version: 1.0 Content-Type: TEXT/PLAIN; charset=US-ASCII Sender: owner-caml-list@pauillac.inria.fr Precedence: bulk *disclaimer* This is a long mail, that probably only polymorphic variant adepts and static typing fanatics (like me) will like. Moreover I strongly doubt that it could be very useful. *end of disclaimer* Hi list, recently there was a very interesting mail about encoding natural numbers as types for static checking of array sizes, list length etc..., cf http://caml.inria.fr/archives/200109/msg00097.html The trick was to use phantom types, and cps style to have a nice type - number visual correspondance. For practice (and with difficulty ...), I implemented a version with polymorphic variants, but no cps (yet) : module Dim : sig type 'a dec val dec : [`U] dec val to_int : 'a dec -> int type 'a digit = [`D0 of 'a | `D1 of 'a | `D2 of 'a | `D3 of 'a | `D4 of 'a | `D5 of 'a | `D6 of 'a | `D7 of 'a | `D8 of 'a | `D9 of 'a ] val d0 : ([< 'a digit ] as 'd) dec -> [`D0 of 'd] dec val d1 : 'a dec -> [`D1 of 'a] dec val d2 : 'a dec -> [`D2 of 'a] dec val d3 : 'a dec -> [`D3 of 'a] dec val d4 : 'a dec -> [`D4 of 'a] dec val d5 : 'a dec -> [`D5 of 'a] dec val d6 : 'a dec -> [`D6 of 'a] dec val d7 : 'a dec -> [`D7 of 'a] dec val d8 : 'a dec -> [`D8 of 'a] dec val d9 : 'a dec -> [`D9 of 'a] dec end = struct type 'a digit = [ `D0 of 'a | `D1 of 'a | `D2 of 'a | `D3 of 'a | `D4 of 'a | `D5 of 'a | `D6 of 'a | `D7 of 'a | `D8 of 'a | `D9 of 'a ] type 'a dec = int let dec = 0 let to_int x = x let mkd n = fun d -> d * 10 + n let d0, d1, d2, d3, d4, d5, d6, d7, d8, d9 = mkd 0, mkd 1, mkd 2, mkd 3, mkd 4, mkd 5, mkd 6, mkd 7, mkd 8, mkd 9 end Then, # open Dim;; # let x120 = (d0 (d2 (d1 dec)));; val x120 : [ `D0 of [ `D2 of [ `D1 of [ `U]]]] Dim.dec = # to_int x120;; - : int = 120 # let x32 = (d2 (d3 dec));; val x32 : [ `D2 of [ `D3 of [ `U]]] Dim.dec = # x120 = x32;; ^^^ This expression has type [ `D2 of [ `D3 of [ `U]]] Dim.dec but is here used with type [ `D0 of [ `D2 of [ `D1 of [ `U]]]] Dim.dec ... type error :) As you can see the number the type encodes is reversed ('cause lack of cps). Now it seems to me that it's a little more expressive this way. For example, we can define a function that will only accept numbers (or work on array size or list size) greater than zero : # let f_nz (x:[< 'a digit ] dec) = to_int x;; val f_nz : [< 'a Dim.digit] Dim.dec -> int = # let x0 = dec and x1 = (d1 dec);; val x0 : [ `U] Dim.dec = val x1 : [ `D1 of [ `U]] Dim.dec = # f_nz x1;; - : int = 1 # f_nz x32;; - : int = 32 # f_nz x0;; ^^ This expression has type [ `U] Dim.dec but is here used with type ([< 'b Dim.digit] as 'a) Dim.dec Type [ `U] is not compatible with type 'a = [< `D0 of 'b | `D1 of 'b | `D2 of 'b | `D3 of 'b | `D4 of 'b | `D5 of 'b | `D6 of 'b | `D7 of 'b | `D8 of 'b | `D9 of 'b] ... type error again :) But we can go further, and allow f to work only with numbers greater than or equal to 5 for example : # type 'a atleast5 = [ `D5 of 'a | `D6 of 'a | `D7 of 'a | `D8 of 'a | `D9 of 'a ] and 'a atmost4 = [`D0 of 'a | `D1 of 'a | `D2 of 'a | `D3 of 'a | `D4 of 'a ];; *identical signature skipped* # let f_atleast5 (x:[< | [< 'a digit ] atmost4 | [< `U | 'a digit ] atleast5 ] dec) = to_int x *big type annotation skipped* # f_atleast5 x32;; - : int = 32 # f_atleast5 x120;; - : int = 120 # f_atleast5 x1;; Toplevel input: # f_atleast5 x1;; ^^ This expression has type [ `D1 of [ `U]] Dim.dec but is here used with type [< `D1 of [< 'b Dim.digit] as 'a] Dim.dec *rest of big type error skipped* ... type error again, yeah :) The idea is to encode (in the function signature) some kind of deterministic finite automaton from the last digit of the number, which decides if the type is valid (= if the number is in the desired range). You can read the type of f_atleast5 as : - let n be the number encoded in the type of x - if the last digit of n is <= 4, then n must be at least 2 digits long (= we don't allow the unit `U to terminate the type) to be >= 5 - if the last digit is >= 5, n is >= 5 (= we allow anything to terminate the type) For fun, lets work with a parameter statically known to encode a number greater than 25 : # type 'a atleast2 = [ `D2 of 'a | `D3 of 'a | `D4 of 'a | `D5 of 'a | `D6 of 'a | `D7 of 'a | `D8 of 'a | `D9 of 'a ] and 'a atleast3 = [ `D3 of 'a | `D4 of 'a | `D5 of 'a | `D6 of 'a | `D7 of 'a | `D8 of 'a | `D9 of 'a ] and 'a atmost2 = [`D0 of 'a | `D1 of 'a | `D2 of 'a ] and 'a atmost1 = [`D0 of 'a | `D1 of 'a ];; *identical signature skipped* # let f_atleast25 (x:[< | [< [< 'a digit] atmost2 | [< `U | 'b digit ] atleast3 ] atmost4 | [< [< 'a digit] atmost1 | [< `U | 'b digit ] atleast2 ] atleast5 ] dec) = to_int x;; *very big type annotation skipped* # f_atleast25 x32;; - : int = 32 # f_atleast25 x120;; - : int = 120 # f_atleast25 x1;; ^^ This expression has type [ `D1 of [ `U]] Dim.dec but is here used with type *very big type skipped* Again, the type of f_atleast25 may be read : - let n be the number encoded in the type of x, with last digits XYZ (that is n >= X * 100 + Y * 10 + Z). Y and Z must exist but X may not exist. - if Z <= 4 then - if Y <= 2 then X exists <-> n >= 25 - if Y >= 3 then true <-> n >= 25 - if Z >= 5 then - if Y <= 1 then X exists <-> n >= 25 - if Y >= 2 then true <-> n >= 25 In the same way we can encode that n should be less than something, or between something and another, or any finite disjunction and conjunction of intervals as the language of DFA is closed under those operations. The function f_atleast120_andlessthan246 is of course left as an exercice to the masochist reader :) Now the questions to the courageous people that are still here : I think the function f_atleast5 and f_atleast25 are impossible to express with the previous solution wich involved 10 different abstract types in Dim signature, am i right ? When I concatenate all the Ocaml code I gave (except the direct calls to the f_* ) in a single file and I compile, it's fine. But when I add : # let _ = f_atleast5 x32 I get : The type of this expression, [ `D2 of [ `D3 of [ `U]]] Dim.dec, contains type variables that cannot be generalized Can someone explain this ? Thanks for your attention :) , Ocaml really is a wonderful programming language. Bye, Nadji PS: If you think my mail was off-topic let me know so I won't bother you ... PPS: Lots of people have some very nice tricks with typing, maybe it would be a good thing to add a section somewhere in the FAQ or the doc for those "typing pearls". These can be very useful to get an intuition of the limits of static typing. For example, some people posted very nice things about dynamic typing trick (Daniel De Rauglaude I think), memo class for objects (Jacques Garrigue I think), of course Xavier Leroy has a bunch of them etc ... ------------------- To unsubscribe, mail caml-list-request@inria.fr Archives: http://caml.inria.fr Bug reports: http://caml.inria.fr/bin/caml-bugs FAQ: http://caml.inria.fr/FAQ/ Beginner's list: http://groups.yahoo.com/group/ocaml_beginners