On 13 June 2015 at 10:47, Matt Oliveri <[email protected]> wrote: > > > The grammar specification in the type checking will be redundant. The > > type-inference specification will be the same as the grammar (the same > > clauses with additional arguments for the types). > > That may appear so, but it's different, since the grammar refers to > surface syntax, whereas a separate set of typing rules would refer to > ASTs, and not involve surface syntax. The cases of the AST type(s) do > not exactly match the cases in the grammar, so a separate grammar is > not redundant. For example, only a grammar would have a case to wrap > an expression in parentheses. Conventional typing rules do not need > that case. >
I see where we disagree now. I do not deal in surface syntax, and I do not like string based formalisms for this. For me the grammar is abstract and hence about the AST that is accepted. If for example we are working in homoiconistic language like Lisp or Prolog, then we can write the AST directly: Lisp: (abs x (var x)) Prolog: abs(x, var(x)) Specifying how strings get converted into the AST representation is the job of the parser. > It may not be worth explaining it yet. There are still simpler things, > like HasTwo, and even10, that I'm waiting for you to address. I can't find a reference to HasTwo, but even10: Inductive Even : nat->Prop := > ez : Even O | > ess n : Even n->Even (S (S n)). > Definition even10 : Even 10 := ess 8 (ess 6 (ess 4 (ess 2 (ess 0 ez)))). I don't really get what you want me to do here? The type level logic program: nat(z). nat(s(X)) :- nat(X). even(z). even(s(s(X))) :- even(X). :- even(s(s(s(s(s(s(s(s(s(s(z))))))))))). yes. So given a value level program: ten :: even a => a ten = 10 this works because '10' has the type s(s(s(s(s(s(s(s(s(s(z)))))))))) as it is a literal. Keean.
_______________________________________________ bitc-dev mailing list [email protected] http://www.coyotos.org/mailman/listinfo/bitc-dev
