4
$\begingroup$

I know in Agda, rewrite is a syntax sugar that desugars to a with abstraction.
For example, if we have (I'm using the Data.Vec from the standard library):

$$ \DeclareMathOperator{Set}{Set} \DeclareMathOperator{xs}{xs} \DeclareMathOperator{where}{where} \DeclareMathOperator{proof}{proof} \DeclareMathOperator{data}{data} \DeclareMathOperator{rev}{rev} \DeclareMathOperator{ff}{ff} \DeclareMathOperator{lemma}{lemma} \DeclareMathOperator{intro}{intro} \DeclareMathOperator{id}{id} \DeclareMathOperator{refl}{refl} \DeclareMathOperator{params}{params} \DeclareMathOperator{Vec}{Vec} \DeclareMathOperator{rewrite}{rewrite} \DeclareMathOperator{with}{with} \DeclareMathOperator{revrevid}{revrevid} \begin{align*} & \revrevid : \forall \{n \ m\} \{A : \Set n\} (a : A) (v : \Vec A \ m) \rightarrow \rev (v \ {:}{:} ^r a) \equiv a \ {:}{:}\rev v \\ & \revrevid \ \_ \ [] = \refl \\ & \revrevid \ a \ (\_ \ {:}{:} \ \xs) \ \rewrite \revrevid \ a \ \xs = \refl \end{align*} $$

This will be desugared to:

$$ \begin{align*} & \revrevid : \forall \{n \ m\} \{A : \Set n\} (a : A) (v : \Vec A \ m) \rightarrow \rev (v \ {:}{:} ^r a) \equiv a \ {:}{:}\rev v \\ & \revrevid \ \_ \ [] = \refl \\ & \revrevid \ a \ (\_ \ {:}{:} \ \xs) \with \ \rev (\xs \ {:}{:}^r \ a) \ | \ \revrevid \ a \ \xs \\ & ... \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | \ {.}(a \ {:}{:} \rev \xs) \ | \refl = \refl \end{align*} $$

But in Idris, there's nothing like a with abstraction, or a dot pattern (which are available in Agda).
So how does Idris' rewrite implemented? Is that just a syntax sugar or a language feature which cannot be implemented in pure Idris code?

$\endgroup$
  • $\begingroup$ Update: Idris do have with abstraction. $\endgroup$ – ice1000 Oct 13 '18 at 7:01
4
$\begingroup$

I talked to be5invis and he said it's implemented using replace.

replace is something like this in Agda: $$ replace : \forall \{a \ b\} \rightarrow (a \equiv b) \rightarrow P \ a \rightarrow P \ b $$ or, using universal polymorphism: $$ replace : \forall \{n\} \{a \ b : Set \ n\} \rightarrow (a \equiv b) \rightarrow P \ a \rightarrow P \ b $$

This is obvious, in both Agda and Idris.

And we use it like this:

$$ \begin{align*} & proof : \ (a \equiv b) \rightarrow P \ a \rightarrow P \ b \\ & proof \ theory \ pa = replace \ theory \ pa \end{align*} $$

While rewrite in is just a mixfix version of replace, so, the code above can be written like this:

$$ \begin{align*} & proof : \ (a \equiv b) \rightarrow P \ a \rightarrow P \ b \\ & proof \ theory \ pa = rewrite \ theory \ in \ pa \end{align*} $$

In conclusion, rewrite is syntax sugar which desugars to replace, while replace is a library function that can be implemented by anyone.
So there's nothing special.

Actually, Idris desugars it to a function like this:

rewrite__impl : (P : a -> Type) -> x = y -> P y -> P x
rewrite__impl P Refl prf = prf
| cite | improve this answer | |
$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

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