Version française
Home     About     Download     Resources     Contact us    
Browse thread
Re: module type constraints question
[ Home ] [ Index: by date | by threads ]
[ Search: ]

[ Message by date: previous | next ] [ Message in thread: previous | next ] [ Thread: previous | next ]
Date: NaN-NaN-NaN (NaN:NaN)
From: Warren Harris <wh232@p...>
Subject: Re: module type constraints question

>>module type Iter =
>>sig
>> type 'a t
>> val iter : ('a -> unit) -> 'a t -> unit
>>end
>>
>>type expr =
>> Expr of expr * expr
>> | Unit
>> 
>>
>
>Logic problem
>Here your iterator is needing to iter on elements. What are the elements of
>expr ??
>
No, I intentionally simplified the expr type for the purposes of 
isolating the problem. My real expr type is much more complicated (and 
useful :-).


>>Values do not match:
>> val iter : (expr -> unit) -> expr -> unit
>>is not included in
>> val iter : ('a -> unit) -> 'a t -> unit
>> 
>>
>
>Well, two types are different. ExprIter.iter takes two argument whose
>types are expr -> unit and expr. To match the constraints of Iter, we
>have to equate expr -> unit and 'a -> unit, which means we have to
>equate expr and 'a. But from the type of the second argument, we have
>to maintain 'a t = expr. So expr expr = expr,
>
I think you mean "expr t = expr" (which is what I was trying to achieve).

> which is impossible
>(unless you use recursive types). I don't have an expert knowledge of
>the type system, but I hope this is not so far off the mark. Anyways,
>your definition of ExprIter is puzzling for me. expr is not
>polymorphic, so if you define type 'a t = expr, essentially you
>discard a type variable 'a. Is it really what you want to do? 
>
Well, I thought so. I tried to specify 'a t to be an expr so that the 
type checker will indeed unify 'a = expr = 'a t, but it seems that 
either I need to specify additional constraints (somehow), or the type 
checker isn't capable of making this inference.

> If you
>want to define
> type 'a expr = Expr of 'a expr * 'a expr
> | Unit of 'a
>as Nicolas suggested, then iter would become
> let rec iter f e =
> match e with
> Expr(a, b) -> iter f a; iter f b
> | Unit e -> f e
>
Although this type checks, it isn't really what I want. The function f 
is supposed to be expr->unit and apply to all expr nodes in the graph, 
not just the 'a leaves. So, something more like this would be appropriate:

type 'a expr =
Expr of int * 'a expr * 'a expr
| Int of int
| Unit

let rec iter f e =
f e;
match e with
Expr(i, a, b) -> iter f a; iter f b
| e -> ()

val iter : ('a expr -> 'b) -> 'a expr -> unit = <fun>



although notice again that 'a doesn't really get used. But when I try to 
cast this into the desired signature, I again get an error:

module ExprIter : Iter =
struct
type 'a t = 'a expr
let rec iter f e =
f e;
match e with
Expr(i, a, b) -> iter f a; iter f b
| e -> ()
end

Signature mismatch:
Modules do not match:
sig type 'a t = 'a expr val iter : ('a expr -> 'b) -> 'a expr -> unit end
is not included in
Iter
Values do not match:
val iter : ('a expr -> 'b) -> 'a expr -> unit
is not included in
val iter : ('a -> unit) -> 'a t -> unit


or, constraining iter's parameters:

module ExprIter : Iter =
struct
type 'a t = 'a expr
let rec iter (f:'a -> unit) (e:'a t) =
f e;
match e with
Expr(i, a, b) -> iter f a; iter f b
| e -> ()
end

f e;
^
This expression has type 'a t = 'a expr but is here used with type 'a


Note that I think these definitions are less correct because they force 
'a expr to be unified with 'a, and that would result in an infinite 
type: expr expr expr.... So defining expr without a type parameter, and 
declaring 'a t = expr seems like the right thing to avoid this problem.

>
>By the way, is there a definition of the condition when structures
>match signatures? I feel the explanation of the online manual (in
>Section 6.10.2) is too terse.
> 
>
I've tried the o'reilly book too, but can't figure out from that what 
additional constraints might be needed here either.

Thanks for your help,

Warren


[Non-text portions of this message have been removed]