DIPARTIMENTO   DI   INFORMATICA
Università di Torino

Rank 2 intersection types for a simple language of modules (built on a subset of Caml) - Examples


Index

  1. Examples taken from [Damiani, 2003b]
  2. Examples involving datatypes

1. Examples taken from [Damiani, 2003b]

  • The modules m_1 and m_2

    Intrachecking the module m_1

    define 
       x = toList 3 
       and
       y = toList true
    ;;
    
    yields the interface i_1
    interface
    defined
       < 
         { 
           toList: (bool -> 'b ^ int -> 'a) 
         };
         { 
           x {toList}: 'a
         , y {toList}: 'b
         }
       >
    end
    
    where
    • all the type variables occuring in the pair
         < 
           { 
             toList: (bool -> 'b ^ int -> 'a) 
           };
           { 
             x {toList}: 'a
           , y {toList}: 'b
           }
         >
      
      are universally quantified (a way to emphasize this would be that of writing the interface as:
      interface
      defined
         forall 'a 'b.
         < 
           { 
             toList: (bool -> 'b ^ int -> 'a) 
           };
           { 
             x {toList}: 'a
           , y {toList}: 'b
           }
         >
      end
      
      however, we have preferred to avoid to write explicitly the universal quantification),
    • the first component of the pair
           { 
             toList: (bool -> 'b ^ int -> 'a) 
           }
      
      specifies the intersection of the simple types required for the occurrences of the undefined identifier "toList" in the module, and
    • the second component of the pair
           { 
             x {toList}: 'a
           , y {toList}: 'b
           }
      
      specifies the rank 2 types inferred for the identifiers "x" and "y" defined in the module - note that each defined identifier is followed by the set of the undefined identifiers occurring in its definition.

    Intrachecking the module m_2

    define 
       toList z = [z] 
    ;; 
    
    yields the interface i_2
    interface
    defined
       < 
         {};
         { 
           toList:	'a -> 'a list
         }
       >
    end
    
    Performing the interchecking of the interfaces i_1 and i_2 (that is runnining the interchecking tool on the interface sequence
    interface
    defined
       < 
         { 
           toList: (bool -> 'b ^ int -> 'a) 
         };
         { 
           x {toList}: 'a
         , y {toList}: 'b
         }
       >
    end
    interface
    defined
       < 
         {};
         { 
           toList:	'a -> 'a list
         }
       >
    end
    ;;
    
    ) yields the interface i_1,2
    interface
    defined
       <
        {};
        {
          x:      int list
        , y:      bool list
        , toList: 'a -> 'a list
        }
       >
    end
    
    which is the same result yielded by the intrachecking of the module m_1,2:
    define 
       x = toList 3 
       and
       y = toList true
       and
       toList z = [z] 
    ;;
    
  • The modules m_4 and m_5

    Intrachecking the module m_4

    define 
       twice f x = f (f x)
    ;;
    
    yields the interface i_4
    interface
    defined
       <
        {};
        {
          twice: ('c -> 'a ^ 'a -> 'b) -> 'c -> 'b
        }
       >
    end
    
    Intrachecking the module m_5
    declare
       twice: (('a -> 'b) ^ ('b -> 'c)) -> 'a -> 'c
    ;;
    define 
       g = twice (fun z -> [z])
    ;; 
    
    (where the type
       (('a -> 'b) ^ ('b -> 'c)) -> 'a -> 'c
    
    declared for "twice" is indeed a closed rank 2 type scheme, i.e., all the type variables occurring in it are universally quantified) yields the interface i_5
    interface
    declared
         twice: { ('c -> 'a ^ 'b -> 'c) -> 'b -> 'a }
    defined
       <
        {};
        {
          g: 'a -> 'a list list
        }
       >
    end
    
    where
         { ('c -> 'a ^ 'b -> 'c) -> 'b -> 'a }
    
    is the set (a singleton set, in this example) of the closed rank 2 type schemes declared for "twice".

    Performing the interchecking of the interfaces i_4 and i_5 yields the interface i_4,5

    interface
    defined
       <
        {};
        {
          twice: ('s -> 'q ^ 'r -> 's) -> 'r -> 'q
        , g:     'w -> 'w list list
        }
       >
    end
    
    which is the same result yielded by the intrachecking of the module m_4,5:
    declare
       twice: (('a -> 'b) ^ ('b -> 'c)) -> 'a -> 'c
    ;;
    define 
       twice f x = f (f x)
       and
       g = twice (fun z -> [z])
    ;;
    
  • The modules m_4 and m_6

    Let m_4 and i_4 be the module and the interface considered above.

    Intrachecking the module m_6

    define 
       h = twice (fun w -> w)
    ;; 
    
    yields the interface i_6
    interface
    defined
       <
        {
          twice: ('a -> 'a) -> 'b
        };
        {
          h {twice}: 'b
        }
       >
    end
    
    Performing the interchecking of the interfaces i_4 and i_6 yields the interface i_4,6
    interface
    defined
       <
        {};
        {
          twice: ('c -> 'a ^ 'b -> 'c) -> 'b -> 'a
        , h:     'i -> 'i
        }
       >
    end
    
    which is the same result yielded by the intrachecking of the module m_4,6:
    define 
       twice f x = f (f x)
       and
       h = twice (fun w -> w)
    ;;
    
  • The modules m_4, m'_5 m_6 and m_7

    Let m_4, i_4, m_6, and i_6, be the modules and the interfaces considered above.

    Intrachecking the module m'_5

    declare
       twice: (('d -> 'd list) ^ ('d list -> 'd list list)) 
              -> 'd 
              -> 'd list list
    ;;
    define 
       g = twice (fun z -> [z])
    ;; 
    
    yields the interface i'_5
    interface
    declared
         twice: { 
      	     ('a list -> 'a list list ^ 'a -> 'a list) 
    	     -> 'a 
    	     -> 'a list list 
                }
    defined
       <
        {};
        {
          g: 'a -> 'a list list
        }
       >
    end
    
    Intrachecking the module m_7
    declare
       twice: (('e -> ('e * int)) ^ (('e * int) -> (('e * int) * int))) 
    	  -> 'e 
    	  -> (('e * int) * int)
    ;;
    define 
       r = twice (fun z -> (z,3))
    ;; 
    
    yields the interface i_7
    interface
    declared
         twice: { 
    	      (('a * int) -> (('a * int) * int) ^ 'a -> ('a * int)) 
    	      -> 'a 
    	      -> (('a * int) * int)
                }
    defined
       <
        {};
        {
          r: 'a -> (('a * int) * int)   
        }
       >
    end
    
    Performing the interchecking of the interfaces i'_5, and i_7 yields the interface i'_5,7
    interface
    declared
     twice: { 
    	  ('a -> 'a list ^ 'a list -> 'a list list) 
    	  -> 'a -> 'a list list
    	, ('a -> ('a * int) ^ ('a * int) -> (('a * int) * int)) 
    	  -> 'a -> (('a * int) * int)
    	}
    defined
       <
        {};
        {
          g: 'a -> 'a list list
        , r: 'c -> (('c * int) * int)
        }
       >
    end
    
    Performing the interchecking of the interfaces i_4, i'_5, i_6, and i_7 (or, since the interchecking operation is associative, the interchecking of the interfaces i_4, i'_5,7, and i_6) yields the interface i'_4,5,6,7
    interface
    defined
       <
        {};
        {
          twice: ('c -> 'a ^ 'b -> 'c) -> 'b -> 'a
        , g:     'e -> 'e list list
        , h:     'm -> 'm
        , r:     'i -> (('i * int) * int)
        }
       >
    end
    
    which is the same (modulo alpha-renaming of bound type variables and permutation of the elements in the second component of the pair following the keyword defined) result yielded by the intrachecking of the module m'_4,5,6,7:
    declare
       twice: (('a -> 'b) ^ ('b -> 'c)) -> 'a -> 'c
    ;;
    define 
       twice f x = f (f x)
       and
       g = twice (fun z -> [z])
       and
       h = twice (fun w -> w)
       and
       r = twice (fun z -> (z,3))
    ;;
    

2. Examples involving datatypes

  • The module m_ThreeValueLogic

    Intrachecking the module m_ThreeValueLogic (which realizes a datatype tvl)

    export 
       type tvl = False | True | Unknown
       ;;
    define 
       notTVL v = match v with False -> True  
    		      | True -> False
    		      | Unknown -> Unknown
       and
       andTVL p = match p with (False, _) -> False
    			 | (_, False) -> False
    			 | (True, True) -> True
    			 | (_, _) -> Unknown
       and
       orTVL p = match p with (True, _) -> True
    			| (_, True) -> True
    			| (False, False) -> False
    			| (_, _) -> Unknown
    ;;
    
    yields the interface i_ThreeValueLogic
    interface
    exported
       type tvl = False | True | Unknown
    defined
        <
         {};
         {
           notTVL: tvl -> tvl
         , andTVL: (tvl * tvl) -> tvl
         , orTVL : (tvl * tvl) -> tvl
         }
        >
    end
    
    Intrachecking the module Test1
    define 
       nandTVL p = notTVL (andTVL p) 
    ;;
    
    yields the interface i_Test1
    interface
    defined
        <
         {
           notTVL: 'a -> 'b
         , andTVL: 'c -> 'a
         };
         {
           nandTVL {notTVL, andTVL}: 'c -> 'b
         }
        >
    end
    
    Intrachecking the module Test2
    import 
       type tvl = False | True | Unknown
       ;;
    define 
       xorTVL p = match p with (False, False) -> False
    			 | (True, True) -> False
    			 | (False, True) -> True
    			 | (True, False) -> True
    			 | (_, _) -> Unknown
    ;;
    
    yields the interface i_Test2
    interface
    imported
       type tvl = False | True | Unknown
    defined
        <
         {};
         {
            xorTVL: (tvl * tvl) -> tvl
         }
        >
    end
    
    Performing the interchecking of the interfaces i_ThreeValueLogic, i_Test1, and i_Test2 yields the interface i_ThreeValueLogic,Test1,Test2
    interface
    exported
       type tvl = False | True | Unknown
    defined
        <
         {};
         {
           notTVL:  tvl -> tvl
         , andTVL:  (tvl * tvl) -> tvl
         , orTVL :  (tvl * tvl) -> tvl
         , nandTVL: (tvl * tvl) -> tvl
         , xorTVL:  (tvl * tvl) -> tvl
         }
        >
    end
    
    which is the same result yielded by the intrachecking of the module m_ThreeValueLogic,Test1,Test2:
    export 
       type tvl = False | True | Unknown
       ;;
    define 
       notTVL v = match v with False -> True  
    		      | True -> False
    		      | Unknown -> Unknown
       and
       andTVL p = match p with (False, _) -> False
    			 | (_, False) -> False
    			 | (True, True) -> True
    			 | (_, _) -> Unknown
       and
       orTVL p = match p with (True, _) -> True
    			| (_, True) -> True
    			| (False, False) -> False
    			| (_, _) -> Unknown
       and
       nandTVL p = notTVL (andTVL p) 
       and
       xorTVL p = match p with (False, False) -> False
    			 | (True, True) -> False
    			 | (False, True) -> True
    			 | (True, False) -> True
    			 | (_, _) -> Unknown
    ;;
    
  • The module m_Queue

    Intrachecking the module m_Queue (which realizes a datatype 'a queue whose values, as specified by the keyword "readonly", cannot be created outside of the module)

    export 
       type readonly 'a queue = Queue of 'a list
       ;;
    define 
       emptyQueue = Queue []  
       and
       enqueue q e = match q with Queue s -> 
    		 let rec addLast l = match l with []       -> [e]
    					   | (h :: t) -> h :: (addLast t)
                      in
    		    Queue (addLast s)
       and
       deleteFirst q = match q with Queue (h :: t) -> Queue t 
    ;;
    
    yields the interface i_Queue
    interface
    exported
       type readonly 'a queue = Queue of 'a list
    defined
        <
         {};
         {
           emptyQueue : 'a queue
         , enqueue    : 'b queue -> 'b -> 'b queue
         , deleteFirst: 'c queue -> 'c queue
         }
        >
    end
    
    Intrachecking the module m_TestQueue (which uses the datatype 'a queue and, as specified by the keyword "readonly", to create values of type 'a queue it has to resort to the operations provided by the module m_Queue)
    import 
       type readonly 'a queue = Queue of 'a list
       ;;
    define 
       lengthOf q = match q with Queue s -> 
    		let rec length l = match l with []       -> 0
    					 | (h :: t) -> 1 + (length t)
                      in
    		    length s
    ;;
    
    yields the interface i_TestQueue
    interface
    imported
       type readonly 'a queue = Queue of 'a list
    defined
        <
         {};
         {
           lengthOf: 'a queue -> int
         }
        >
    end
    
    Performing the interchecking of the interfaces i_Queue and i_TestQueue yields the interface i_Queue,TestQueue
    interface
    exported
       type readonly 'a queue = Queue of 'a list
    defined
        <
         {};
         {
           emptyQueue  : 'b queue
         , enqueue     : 'c queue -> 'c -> 'c queue
         , deleteFirst : 'd queue -> 'd queue
         , lengthOf    : 'f queue -> int
         }
        >
    end
    
    which is the same result yielded by the intrachecking of the module m_Queue,TestQueue:
    export 
       type readonly 'a queue = Queue of 'a list
       ;;
    define 
       emptyQueue = Queue []  
       and
       enqueue q e = match q with Queue s -> 
    		 let rec addLast l = match l with []       -> [e]
    					   | (h :: t) -> h :: (addLast t)
                      in
    		    Queue (addLast s)
       and
       deleteFirst q = match q with Queue (h :: t) -> Queue t 
       and
       lengthOf q = match q with Queue s -> 
    		let rec length l = match l with []       -> 0
    					 | (h :: t) -> 1 + (length t)
                      in
    		    length s
    ;;
    
  • The module m_Stack

    Intrachecking the module m_Stack, which realizes an abstract type 'a stack (the type is abstract since, as specified by the keyword "opaque", the costructors are not visible outside of the module),

    export 
       type opaque 'a stack = Stack of 'a list 
    ;;
    define 
       emptyStack = Stack []  
       and
       top s = match s with Stack (h :: t) -> h 
       and
       pop s = match s with Stack (h :: t) -> Stack t 
       and
       push e s = match s with Stack l -> Stack (e :: l)
       and
       isEmpty s = match s with Stack [] -> true
    			  | _        -> false
    ;;
    
    yields the interface i_Stack
    interface
    exported
           type opaque 'a stack
    defined
       <
        {};
        {
          emptyStack: 'a stack
        , top:        'b stack -> 'b
        , pop:        'c stack -> 'c stack
        , push:       'd -> 'd stack -> 'd stack
        , isEmpty:    'e stack -> bool
        }
       >
    end
    
    Intrachecking the module m_TestStack
    define 
       test = isEmpty (pop (push 3 emptyStack)) 
    ;; 
    
    yields the interface i_TestStack
    interface
    defined
       <
        {
          pop: 'a -> 'b
        , isEmpty: 'b -> 'c
        , emptyStack: 'd
        , push: int -> 'd -> 'a
        };
        {
          test {isEmpty, pop, push, emptyStack}: 'c
        }
       >
    end
    
    Performing the interchecking of the interfaces i_Stack and i_TestStack yields the interface i_Stack,TestStack
    exported
           type opaque 'a stack
    defined
       <
        {};
        {
          emptyStack : 'b stack,
        , top        : 'c stack -> 'c
        , pop        : 'd stack -> 'd stack
        , push       : 'e -> 'e stack -> 'e stack
        , isEmpty    : 'f stack -> bool
        , test       : bool
        }
       >
    end
    
    which is the same result yielded by the intrachecking of the module m_Stack,TestStack:
    export 
       type opaque 'a stack = Stack of 'a list 
    ;;
    define 
       emptyStack = Stack []  
       and
       top s = match s with Stack (h :: t) -> h 
       and
       pop s = match s with Stack (h :: t) -> Stack t 
       and
       push e s = match s with Stack l -> Stack (e :: l)
       and
       isEmpty s = match s with Stack [] -> true
    			  | _        -> false
       and
       test = isEmpty (pop (push 3 emptyStack)) 
    ;;
    

BIBLIOGRAPHY



[Back]

Comments to: damiani[at]di[dot]unito[dot]it