[clean-list] Fw: Curry type assignment algorithm question

[Jigang Sun]

Hi,

I feel chapter 6 Type Assignment System Functional of Rinus book Programming and Parallel Graph Rewriting is not well understood with no much detailed explanation or example to algorithms. 

Attached is my work using Curry_type Assignment algorithm on λx.x. The result is obviously wrong:the basis I got is empty set, final type is φ1-> φ1 other than φ0-> φ0. 

Could anyone point out what is wrong with my deduction? Do any have other easy learning materials containing explanations or examples for type assignment?

Many thanks.

Jigang 


Curry: [φ0, φ1, φ2, φ3…] λx.x 
= (ftvs’, basis, s φ0->τ)
=> ([φ2, φ3…], [], (sub φ0 φ1) φ0-> φ1)
=> ([φ2, φ3…], [], φ1-> φ1)


Where 
(basis,s)=check_assmptn ( x, φ0) bas
	=> check_assmptn ( x, φ0)  [(x, φ1)]
	=>check_assmptn ( x, φ0)  [ (x, φ1):[] ]
	=> (substitute (s2•s1) bas1, s2•s1 )  )   //because x==x
	=> (substitute (s2•(sub φ0 φ1)) bas1, s2• (sub φ0 φ1) )) 
	=> (substitute (s2•(sub φ0 φ1)) [], s2• (sub φ0 φ1) ))
	=> (substitute ((identisub • (sub φ0 φ1)) [] , identisub • (sub φ0 φ1)  )
=> (substitute (sub φ0 φ1)  [] ,identisub (sub φ0 φ1)) 
	=> ([],identisub (sub φ0 φ1))
	=> ([],sub φ0 φ1)

	Where s1=unify φ0 φ1
		  =>sub φ0 φ1

		(bas1, s2)=check_assmptn(x, s1 φ0) []  //rest is empty 
  =>([], identisub) 
		

(ftvs’,bas, τ) =curry [φ1, φ2, φ3…]  x
		=> ([φ2, φ3…], [(x, φ1)], φ1)



-------------- next part --------------
An embedded message was scrubbed...
From: "Jigang Sun" <js035288 at student.paisley.ac.uk>
Subject: Curry type assignment algorithm question 
Date: Tue, 13 Sep 2005 20:53:12 +0100
Size: 38364
Url: http://mailman.science.ru.nl/pipermail/clean-list/attachments/20050913/c9650919/attachment-0001.mht