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

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?

• Please make your code fragments complete, presumably they are using some package for the software in question but is that available in texlive or ctan or.... Apr 2, 2014 at 9:06
• Updated question to include a complete runnable example. Apr 2, 2014 at 9:11
• It would be nice if someone could create a tag for lhs2TeX, because there are already about 15 questions that are very closely related to lhs2TeX. Apr 2, 2014 at 9:14
• So I created the tag, but I don't know what it is:-) I'll google for it and add some words in a bit:-) Apr 2, 2014 at 9:21
• lhs2TeX is a preprocessor for TeX available at andres-loeh.de/lhs2tex. Most commonly it uses the polytable package to format Haskell code using TeX directives while allowing the source to be reused as a literate Haskell program. Thus the lhs2TeX tag is somewhat related to the literate-programming tag. Apr 2, 2014 at 9:26

2 Answers

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.)

• Elegant solution. Would you use the same solution for Agda where one would have to repeat the type signature for somefunction0? Apr 3, 2014 at 11:37
• @Helmut For Agda, I'd probably use somefunction0 for the type signature at that point, and add another %if False-hidden type signature before the later definition. Apr 3, 2014 at 11:40
• One can also verify that these functions have the same type by adding a list of them somefunctions_have_common_type = [ somefunction, somefunction0 ]. Apr 10, 2014 at 14:00

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}