Hello, Last night I thought to use the System F embedded at the Ur/Web type/kind level to Girard encode some basic datatypes. From the Ur Reference Manual I think we write polymorphic "pi types" with -->, so that in the Boolean case pi t. t -> t -> t we write B --> B -> B -> B in Ur/Web and that we write polymorphic abstraction ( upper case lambda = \\ , lower case lambda = \ ) \\t . \x : t . x as K ==> fn ( x :: K ) => x in Ur/Web.
However, this does not compile: con btrue = K ==> fn ( x :: K ) ( y :: K ) => x con bfalse = K ==> fn ( x :: K ) ( y :: K ) => y con bnot = fn ( b :: (B --> B -> B -> B) ) => K ==> fn ( x :: K ) ( y :: K ) => b y x con bnottrue = bnot btrue giving error message Wrong kind Constructor: (fn x :: <UNIF:U116> => (fn y :: <UNIF:U116> => x)) Have kind: <UNIF:U116> -> <UNIF:U116> -> <UNIF:U116> Need kind: B --> B -> B -> B Incompatible kinds Kind 1: <UNIF:U116> -> <UNIF:U116> -> <UNIF:U116> Kind 2: B --> B -> B -> B >From the error message ( incompatible kinds when as I understand it they should be compatible ) I think this is an example of incompleteness in the kind unification. But I am not sure I am properly writing bnot in Ur/Web ... I am trying to write bnot = \b : Bool . \\t . \x : t . \y : t . b [t] y x where Bool is pi t. t -> t -> t and the \\, \ are uppercase, lowercase lambda. Is this unification incompleteness or am I doing something wrong? _______________________________________________ Ur mailing list [email protected] http://www.impredicative.com/cgi-bin/mailman/listinfo/ur
