Support parsing ' used to promote types to kinds.

[goldfirere]

I use lhs2TeX for all my papers. It's wonderful.

But it can't parse ' in Proxy :: Proxy 'True! My solution has been to have %format ! = "\mathop{}\tick" but then I need to remember to use ! instead of ' in my code. And I have to define the action on ! separately for any operators, such as !:. The input ![] (correctly) does not parse as an operator, so I need %format nil = "\tick" [] and then remember to use nil. Then, I want to be able to compile my papers, so I need translations when style == newcode, as well. But the output cannot have ' in it, because that confuses lhs2TeX. So instead I have the output contain TICK and then use a perl script to replace TICK with '. (Yes, I know sed or awk or some such tool is more well-suited than perl here. But perl has the distinct advantage in that I already know how to use it.)

These workarounds do work, even at scale. But it would be great not to have to work around.

Thanks!

[kosmikus]

I don't think you need perl / awk / sed. You can do everything with formatting directives that are producing different output depending on whether you're in poly or newcode mode.

Probably you're missing the info that you can escape quotes on the RHS:

%if style == newcode
%format | = "''"
%endif

You're also right, of course, that it would be nice to avoid all these hacks. As it's likely we're going to add a third lexer language (see #49) next to Haskell and Agda, perhaps we could add Dependent Haskell as well and implement it in that mode.

[goldfirere]

Ah. I didn't know that "''" would produce a single tick-mark in the output. That will greatly simplify. Thanks.

As far as a new lexer: I don't think we're ready to have a Dependent Haskell lexer. Instead, the Haskell lexer should be taught that a single quote followed by a character followed by anything other than a single quote does not begin a character literal. I believe that's how GHC's lexer does it. For example, if we have data T = A | B and now I want a type of kind [T], I can't write '['A, 'B] because the '[' gets lexed as a character. Instead, I have to use '[ 'A, 'B].

Perhaps such a rule would be difficult in lhs2TeX's lexer, of course -- but I don't think a whole separate lexer is warranted here.

[kosmikus]

It wouldn't necessarily be entirely different. It would just mean that it's an extra flag, and not active by default.

[ivanperez-keera]

Thanks for the tip about "''", @kosmikus . I was using \textquotesingle, which produced lots of warnings. However, "''" does not leave a space before (which might or might not have been there in the first place). Is there any way of addressing that so that a space appears before only if it was in the code?

I agree with you both that it would be great to have this. The whole point of using lhs2tex (at least for me) is to be able to compile these files and know the implementation and the paper are consistent. Most of my papers are not valid haskell at the moment due to these workarounds.

Is this feature hard to add? (I am not assuming it isn't, I'm honestly asking if it would require a lot of work.)

[kosmikus]

The spacing problem is triggered if you use a symbol to expand to the quote, because lhs2TeX's lexer does not properly guess that the quote is a unary operator.

Something like this should have better spacing behaviour:

%format (QUOTE x) = "''" x

[goldfirere]

My workarounds already working, I haven't updated them to use "''". But I imagine @ivanperez-keera's problem can be solved with "\mathop{}''" which looks to leave the right amount of space.

[kosmikus]

That'll probably leave too much space under certain circumstances, but sure, if it works for you, then great :)