1

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?

6
  • 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.
    – Helmut
    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.
    – Helmut
    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.
    – Helmut
    Apr 2, 2014 at 9:26

2 Answers 2

2

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

3
  • Elegant solution. Would you use the same solution for Agda where one would have to repeat the type signature for somefunction0?
    – Helmut
    Apr 3, 2014 at 11:37
  • 1
    @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.
    – kosmikus
    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 ].
    – Helmut
    Apr 10, 2014 at 14:00
1

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}

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.