On Sun, 2006-09-03 at 09:49 +1000, skaller wrote:
>
> My typematch also fails for a different reason:
>
> ---------------------------------------
> typedef fun ite2(b:TYPE, s:TYPE, r: TYPE): TYPE =>
> typematch b with
> | True => s
> | False => r
> endmatch
> ;
>
> var dum11: ite2 (True, int, long) = 1; // int
>
> [lookup_name_in_env]: Name 's' not found in environment (depth 2)
> In a.flx: line 120, cols 13 to 13
> 119: typematch b with
> 120: | True => s
> *
> 121: | False => r
> -------------------------------
>
> Woops, looks like I messed up the environment construction
> (s is of course a parameter, so it is a bound variable,
> the diagnostic is saying it is a free variable .. :)
Yup, fixed: typematch works.
Now here is the problem, in flx_beta.ipk:
| `BTYP_apply (t1,t2) ->
let t2 = br t2 in (* eager evaluation *)
let t1 = br t1 in (* eager evaluation *)
So given this function:
typedef fun ite(b:TYPE, s:TYPE, r:TYPE): TYPE =>
typecase [] True =>
typecase [x] x => s endcase
endcase
b r
;
and this test case:
var dum1: ite (True, int, long) = 1; // int
the application of ite (Tre, int, long) is done by reducing ite and
the arg first. Later we do this:
begin match t1 with
| `BTYP_typefun (ps,r,body) ->
let v = Hashtbl.create 97 in
begin match ps with
| [] -> ()
| [i,_] -> Hashtbl.add v i t2
| _ ->
let ts = match t2 with
| `BTYP_type_tuple ts -> ts
| _ -> assert false
in
if List.length ps <> List.length ts
then failwith "Wrong number of arguments to typefun"
else List.iter2 (fun (i,_) y -> Hashtbl.add v i y) ps ts
end
;
let t = varmap_subst v body in
br t
The first part of this decodes the lambda form of a function,
converts the parameter list to a hashtable mapping parameters ps
to argument ts, and substitutes these into the body.
Peter note the matching:
| `BTYP_type_tuple ts -> ts
is looking for the famous 'type tuple' which is quite distinct
from `BTYP_tuple _ constructor. The function is called like:
ite2 (True, int, long)
The RHS is a tuple: were this an executable expression we'd use the
constructor
`BEXPR_tuple _
which is a value. However since we're working in the type system,
we need the equivalent value in the type domain.
The *problem* is that the reduction code is eagerly reducing everything.
I just reduce left right and centre: the code assumes confluence.
So why the heck does my typematch WORK??
The answer is in the sneaky algorithm :)
First for each case we do:
match maybe_unification syms.dfns [p',tt] with
| Some _ -> new_matches := x :: !new_matches
| None -> ()
and then we do:
| ({pattern=p';pattern_vars=dvars;assignments=eqns},t') :: _ ->
try
let mgu = unification false syms.dfns [p', tt] dvars in
let t' = list_subst eqns t' in
list_subst mgu t'
with Not_found -> `BTYP_type_match (tt,pts)
The FIRST unification is ordinary unification.
The SECOND unification is unification with a constraint that only
bindings to the dependent variables are allowed: these are
the LHS variables, this constraint turns the unification
into match.
So the algorithm says: chuck out all the cases that don't
unify. If two expressions don't unify, no substitution
on either side will ever lead to them unifying.
Of the remaining case that do unify, examine ONLY the
very first one. If this generates a match, apply the
unifier to the argument and return it.
If there is no match, return the whole typematch intact,
but minus the cases that can never unify.
The reason is: we know the match MIGHT lead to match
later, even though it doesn't match now: delay processing
because a possible substitution in the argument which enriches
its structure, may allow a match later.
Now here's the funny thing: my representation of a type pattern
is given by:
tpattern_t =
[
| `TPAT_function of tpattern_t * tpattern_t
| `TPAT_sum of tpattern_t list
| `TPAT_tuple of tpattern_t list
| `TPAT_pointer of tpattern_t
| `TPAT_void
| `TPAT_var of string
| `TPAT_name of string * tpattern_t list
| `TPAT_as of tpattern_t * string
| `TPAT_any
| `TPAT_unitsum of int
| `TPAT_type_tuple of tpattern_t list
]
This is very close to the variant for an actual type,
but with 'any' (wildcare) and 'as' (fixpoint binder) added.
But in a type match .. this pattern is NOT used: during binding
I do this:
let p',explicit_vars,any_vars, as_vars, eqns =
type_of_tpattern syms p'
in
let p' = bt p' in
pts := (
{
pattern=p';
pattern_vars=varset;
assignments=eqns
}
,
t'
) :: !pts;
which forms a list of 'dissected patterns'. The 'pattern' is actually
represented in bound form by a bound type, plus a list of pattern
variables plus some assignments (which come from the 'as' terms).
In other words .. my technology ALREADY implements something
like the pattern calculus, and what's more an enriched form of it
(due to the additional assignments).
The difference in the implementations is the 'sneaky algorithm':
for my pattern matching, this appears to serve to delay reduction.
The pure pattern calculus has some 'matchable forms' stuff
which is not implemented which would do the same: my implementation
of it fails because of this .. it prematurely gets a match
failure and returns identity function, causing the case to be
dropped and the next one considered.
In particular note that in my code you see this line:
let pts =
map (fun (tp,t) ->
{
tp with pattern=br tp.pattern;
assignments= map (fun (j,t) -> j, br t) tp.assignments
}, br t
)
pts
in
particularly seeing this one:
tp with pattern=br tp.pattern;
which implies the pattern IS actually reduced. So actually I would
claim that
fun (a)=> typematch a with | m => r endmatch
is already the pattern calculus combinator
typecase [vars_of m] m => r endmatch
so the only difference is that in my form an explicit pattern
is parsed and used to identify the variables, and the shape
of this pattern acts as a limitation: Jay removes that limitation.
--
John Skaller <skaller at users dot sf dot net>
Felix, successor to C++: http://felix.sf.net
-------------------------------------------------------------------------
Using Tomcat but need to do more? Need to support web services, security?
Get stuff done quickly with pre-integrated technology to make your job easier
Download IBM WebSphere Application Server v.1.0.1 based on Apache Geronimo
http://sel.as-us.falkag.net/sel?cmd=lnk&kid=120709&bid=263057&dat=121642
_______________________________________________
Felix-language mailing list
[email protected]
https://lists.sourceforge.net/lists/listinfo/felix-language
