How to mix lhs2TeX code and spec lines in a single block?

Question

Suppose I have an incomplete code block like:

\documentclass{article}
%include polycode.fmt
\begin{document}
\begin{code}
somefunction :: a -> a
\end{code}
\begin{spec}
somefunction x = undefined
\end{spec}
\end{document}

It is supposed to express a work in-progress, because somefunction is only defined at a later point, so I want to hide this incomplete definition from ghc, but I want to reuse the type signature. Unfortunately in this setup there is a vertical space between the two lines. A workaround is to rewrite the document body as follows:

\begin{spec}
somefunction :: a -> a
somefunction x = undefined
\end{spec}
%if False
\begin{code}
somefunction :: a -> a
\end{code}
%endif

This has the downside of being repetitive and thereby likely to introduce mistakes.

The space inserted appears to be about \belowdisplayskip + \baselineskip + \abovedisplayskip, so one could add negative \vspace in the former definition.

Is space really the sum of the above? What solution is recommended for gluing code and spec environments?

Answer 1

The recommended solution in this case would be something like this:

\documentclass{article}
%include polycode.fmt
\begin{document}
%format somefunction0 = somefunction

> somefunction :: a -> a
> somefunction0 x = undefined

Much later:

> somefunction = id

\end{document}

This has the advantage that even the preliminary code is still typechecked when run through GHC. (The use of > instead of code and < instead of spec isn't relevant, but as you were complaining about noise, I thought it might be worth pointing out. Blank lines around code/spec blocks in this style are required.)

Answer 2

Based on kosmikus solution, let me give an extended solution for Agda that avoids repeating the type signature. (Slightly too long for a comment.) It needs a bit more setup code:

\documentclass{article}
%include agda.fmt
\begin{document}
%if False
\begin{code}
open import Reflection
termoftype : Type → Term
termoftype (el s t) = t
\end{code}
%endif

Then we can reuse kosmikus technique:

%format somefunction0 = somefunction
\begin{code}
somefunction0 : {a : Set} → a → a
somefunction0 x = ?
\end{code}

Rather than writing the (possibly long) type signature again, we can obtain it by reflection now:

Much later:
%if False
\begin{code}
somefunction : unquote (termoftype (type (quote somefunction0)))
\end{code}
%endif
\begin{code}
somefunction = id
\end{code}
\end{document}