2
$\begingroup$

I'm reading Wadler's paper called "How to make adhoc polymorphism less ad hoc". I'm trying to understand the given rules for function overload (over and inst) and I want to create a small example of a proof tree using them. All deductions rules are in Figure 9 and Figure 10.

I decided to proof the following expression/type: $(over\: eq:: Eq\: \alpha\: in\: inst\: eq :: Eq\:Int \:=\: eqInt\: in\: eq\:1\:2)::Bool$.

Some people gave me a tip: construct the tree in bottom-up.

So here is what I did: Tree proof

I think I'm stuck. I have no idea how to go up in the tree. And I'm not sure if I can, at some point, discharge the assumption about $eqInt$.

I would like to know what I'm doing wrong and how to finish this proof.


EDIT: As said in the paper, $Eq\: \tau$ is a abbreviation for $\tau \rightarrow \tau \rightarrow Bool$.

$\endgroup$
1
$\begingroup$

After some time I realized that is not possible to proof \begin{align*} \vdash (over\: eq:: Eq\: \alpha\: in\: inst\: eq :: Eq\:Int \:=\: eqInt\: in\: eq\:1\:2)::Bool \end{align*} without suppositions about $1$, $2$ and $eqInt$ ( $\emptyset$ as the context). They need to be bound to the context , because they should be seen as build in to the system. In alternative I could create new rules (like $const$ rules) for the integer numbers ($1$, $2$...) and for $eqInt$, that don't insert stuff to the context.

So, my final result is this proof tree: enter image description here

I'm not sure if I can use $weakening$ in the context, but I did.

I hope that some one could comment something about my answer. If I'm right or if I created some non-sense.

$\endgroup$

Your Answer

By clicking "Post Your Answer", you acknowledge that you have read our updated terms of service, privacy policy and cookie policy, and that your continued use of the website is subject to these policies.

Not the answer you're looking for? Browse other questions tagged or ask your own question.