STLC icon indicating copy to clipboard operation
STLC copied to clipboard

Published 20 hours ago • verified publisher icon effectfully

`M` should be a total decider instead of a partial prover

Open gergoerdi opened this issue 9 years ago • 2 comments

From its type, it seems for a given term, M Maybe gives you a proof of well-typed-ness; but you always have the danger of leaving Nothing-handed.

I think it'd be nicer if M never had the option to wuss out, and it had to Decide well-typed-ness; see e.g. http://gergo.erdi.hu/blog/2013-05-01-simply_typed_lambda_calculus_in_agda,_without_shortcuts/html/STLC.Typecheck.html#2606

gergoerdi avatar Nov 25 '15 06:11 gergoerdi

My primary goal was "to make things work", so the idea about Dec didn't even come to my mind. Thanks for the suggestion, I'll try to make M a decision procedure after I remove some bottoms from the code.

effectfully avatar Nov 25 '15 07:11 effectfully

Hmm.. but I'll probably need first-order unification, which doesn't look efficient at all. Maybe I should write a total version and use the partial for tests.

effectfully avatar Nov 25 '15 07:11 effectfully