> module Intro where
Hello! If you were wondering what happened to me and why I've stopped posting, well, I was found guilty on type abuse charges and was sentenced to three months in maximum type security prison of Coq. Since I'm such a degenerate, I've loved every minute of it. And there were plenty of things to abuse on the inside. Now, I've been released, but I can't believe how fast things move on the outside. I saw an automobile once when I was a kid, but now they're everywhere. And SPJ thinks that OverlappingInstances are unsound. It's been a while, since I made a new post, so I decided, that because of recent events I could make a new post.
Over a year ago, this post was all the rage on reddit. The original implementation used C++ and redditors contributed code in such godless languages like Python and Ruby. There was no Haskell solution and we can't have that, can we? I'm going to present two solutions, to prove that it's possible in ML-like languages, and by using Haskell extensions, it's possible to have some advantages over the original implementation. I've limited myself only to rectangles, because lines are boring and cuboids are too hard to even "draw". Here's an example for the impatient:
rectangle = begin
o ᜭ ᜭ ᜭ ᜭ o
ǀ ǀ
ǀ ǀ
o ᜭ ᜭ ᜭ ᜭ o
endIf it looks broken, it's because it uses two unusual unicode characters (like "LATIN LETTER DENTAL CLICK"), if your browser or font (or my mad web skills) can't handle it, here's a picture.
What's so hard about Haskell implementation of those literals? In languages with ML-like syntax, there can't be two operators next to each other and there are no (usable) postfix operators, so the original idea of overloading decrement and subtraction operators fails already on the syntax level. Unless we want to alternate glyphs between operators and identifiers, which seems a bit against the spirit of this hack, it's clear that the solution has to rely on a sequence of single-char combinators, delimited with spaces (otherwise it would be just one token). It helps if those combinators use letters, that look like operators (it's possible in GHC).
> module PostCombinator(post) where
Before we start, let's talk about this programming style, that I like to call applicative pointfree/pointless. Here's couple functions to calculate reversed list of odd squares:
> square x = x*x
> odds = filter odd
> squares = map square
> oddSquares1 xs = reverse (odds (squares xs))
> oddSquares2 xs = reverse $ odds $ squares xs
> oddSquares3 = reverse . odds . squares
It's composed of three sub-programs in a good functional style. Category-theory guys would tell you, that the third one is pointfree, but you don't have to be a rocket-scientist to notice, that it's the only solution actually containing points. But don't tell that to CT people, they will answer "does not commute!" and their head will explode. The common thing about those functions is this: sub-expressions are delimited or explicitly composed (be it with '.', '$' or opening paren). It would be nice, to be able to write only function names, without any boiler-plate in between, and make it magically combine itself.
I've discovered a way to achieve this goal. It's really beautiful, it's based on very smart people results, there are continuations involved and it has interesting connections with concatenative languages like Factor - all the ingredients of a great paper. Unfortunately (for me), Chris Okasaki already took care of it - Techniques for Embedding Postfix Languages in Haskell. I encourage you to read it yourself, but here's a quick roundup of this technique.
We want a function odds', that will be able to use directly the immediately following sub-program, without any composition means. It must take two arguments: x - the usual input and k - the continuation (Okasaki calls it a partial continuation) that is, the next expression. The following order of those arguments is the easier one:
odds' x k = ...On the right hand side, the obvious thing to do with x is to filter odd numbers from x:
odds' x k = ...
where y = filter odd xNow, we have an output of this sub-computation, the only sensible thing to do is to apply it to the next computation:
> odds' :: [Int] -> ([Int] -> t) -> t
> odds' x k = k y
> where y = filter odd x
> squares', doubles' :: [Int] -> ([Int] -> t) -> t
> squares' x k = k y
> where y = map square x
> doubles' x k = k $ map (*2) x
Now we can compose these expressions:
*PostCombinator> :t odds' [1..10]
odds' [1..10] :: ([Int] -> t) -> t
*PostCombinator> :t odds' [1..10] squares'
odds' [1..10] squares' :: ([Int] -> t) -> t
*PostCombinator> :t odds' [1..10] squares' doubles'
odds' [1..10] squares' doubles' :: ([Int] -> t) -> tIn order to not make special case of the first part, by applying to it the initial state, that gets transformed by the whole pipeline, we can add special combinator, that will apply that initial state to the first case:
> begin x k = k x
We finish the pipeline computation by adding the final continuation, e.g. id, but any other function would be fine too.
*PostCombinator> (begin [1..10]) odds' squares' doubles' id
[2,18,50,98,162]I call this style applicative pointfree, because composition is based on application and there are no points, or any other delimiters.
We can abstract the pattern from odds', squares' and doubles' functions. Okasaki calls this combinator post:
> post :: (a -> b) -> a -> (b -> t) -> t
> post f = \x k -> k $ f x
Explicit usage of post, while possible, doesn't make much sense, because you still have to use parens, it's better suited for creating wrappers around simple functions.
*PostCombinator> begin [1..10] (post$ filter odd) (post$ map square) (post$ map (*2)) reverse
[162,98,50,18,2]If you want to learn more about this style, you should read Techniques for Embedding Postfix Languages in Haskell, Flattening combinators: surviving without parentheses and the classic Functional Unparsing wouldn't hurt either, because it lays the foundations. But be careful, you don't want to start coding in Factor.
> module DynamicLiterals where
The first solution is very simple, it should work in any ML-like language (I've tested it in Haskell and OCaml), because it only requires Hindley-Milner type system. If the implementation doesn't support unicode identifiers, rectangles have to be drawn with other characters though. I call it dynamic solution, because though it does work for correct rectangles, it produces wrong results (at runtime) for wrong combinator sequences, that don't represent rectangles.
> import PostCombinator
There are three different parts of a rectangle and each gets a combinator. These combinators will transform the rectangle state, consisting of width, current width and height (shortened to w,cw and h respectively):
> type RectState = (Int, Int, Int)
> corner, dash, bar :: RectState -> RectState
> dash (w, cw, h) = (w, cw + 1, h)
> bar (w, cw, h) = (w, cw, h + 1)
> corner (w, cw, h) = (w `max` cw, 0, h)
dash and bar are obvious, corner takes maximum of width and current width to account for transition from sequence of bars (that didn't touch current width) to corner.
We wrap these functions with our post combinator:
> c, d, b :: RectState -> (RectState -> t) -> t
> c = post corner
> d = post dash
> b = post bar
All that's left are definitions of the first combinator, that starts the process, and the final continuation:
> beginRect :: (RectState -> t) -> t
> beginRect k = k (0, 0, 0)
> endRect :: RectState -> (Int, Int)
> endRect (w, cw, h) = (w, h `div` 2)
Now we can draw pretty rectangles:
> rect = beginRect
> c d d d d c
> b b
> b b
> b b
> c d d d d c
> endRect
*DynamicLiterals> rect
(4,3)Unfortunately, since there are no requirements on these combinators, they will be perfectly happy to transform any sequence of rectangle states:
> lambda = beginRect
> d
> b d
> b
> d d
> d d b
> d c
> endRect
*DynamicLiterals> lambda
(7,1)It's worth mentioning that this solution (and the next one) doesn't scale - the types are huge, in the smallest proper rectangle (1x1), the first corner combinator c has a type, that takes over 250 lines when printed by ghci. This makes type checking extremely slow for bigger examples. Memory usage varies by implementation, ghc for 4x4 rectangle needs 500 mb of memory (I don't have a machine capable of checking 5x5), while OCaml still takes a long time to compute the type, but it doesn't use any significant amount of memory.
Now it's time for the second solution. This is Haskell after all, find a problem and make it statically impossible to violate. There will be also a few advantages over original C++ implementation.
While we can't forbid drawing rectangles like the lambda letter, because there's no access to the lexer at the type level (but can you imagine the possibilities?), we can forbid usage of incorrect sequences (e.g. dash following bar). This of course needs a bit of type level programming, but there's nothing really hacky and abusive.
> {-# LANGUAGE NoMonomorphismRestriction
> , OverlappingInstances
> , FlexibleInstances
> , FlexibleContexts
> , UndecidableInstances
> , ScopedTypeVariables
> , MultiParamTypeClasses
> , FunctionalDependencies
> , EmptyDataDecls
> #-}
Base implementation only uses MPTCs+FunDeps (and UndecidableInstances, but I'm pretty sure this could be solved without them), so it's probably doable with all those new hip TypeFamilies. OverlappingInstances and UndecidableInstances are needed for nice error messages though, but don't worry, any instance choice, that requires UndecidableInstances will result in a type error - but a pretty one!
> module StaticLiterals where
> import Prelude hiding (Either(..))
> import Peano
Let's take a look at the type of the dash combinator from the previous solution:
d :: RectState -> (RectState -> t) -> tOne of the situations, we wish to forbid, is having bottom side of different length than the top side. This clearly requires tracking rectangle's width at the type level. Since we have to carry the rectangle state through types, there's no need to carry it at the value level, so the RectState argument isn't needed anymore. So, we're left with (t) -> t, and we have to attach type-level equivalent of RectState.
The first t is the continuation. The problem is, that it takes any continuation, so dash followed by bar type checks just fine. Since all three combinator have the same type, we have to do something to be able to distinguish between them. We're going to wrap every continuation type in a newtype wrapper with a phantom type tag, telling what kind of combinator this is.
> data Corner
> data Dash
> data Bar
> data End
Besides width, current width and height we have to carry a position in the rectangle, because e.g. dash can follow the first corner, but it cannot follow the second. Our type level state will be a 4-tuple of 3 Peano numbers and a position.
> data Top
> data Bottom
> data Left
> data Right
> data TopLeft
> data TopRight
> data BottomLeft
> data BottomRight
Our continuation wrapper:
> newtype TagCont tag rectState k = TagCont { unTagCont :: k }
Now it's time for some type level computations, this is the only class (unfortunately, /dev/meaningfull_names run out of entropy). This class contains the combinator, that will work like all three, because interesting things will happen only at the type level. This class is parameterized by the tag of the combinator, the tag of the following combinator, the type level rectangle state input, and those arguments determine the resulting state.
> class Rectangly tag nextTag inpState outState | tag nextTag inpState -> outState where
The r combinator is still of that t -> t type, but that function is tagged with the combinator tag (e.g. Dash), and the inner (left) t is tagged with the tag of the next combinator. State of one combinator determines (together with tags) the state of the following (next) one.
> r :: TagCont tag inpState (TagCont nextTag outState t -> t)
At the value level, all combinators work the same, just tag untagging function, so if we disregard newtypes with phantom arguments, this is just identity function, where everything interesting is happening at the type level.
> r = TagCont unTagCont
All the instances follow the same pattern: dispatching on the rectangle part, tag of the current combinator, tag of the next combinator, accepting any width, current width and height, and computing from that resulting values and next rectangle part.
This one says, that after Corner we can use Bar, but only in the TopRight part (it's certainly not true at any other corner). Current width (calculated by sequence of dashes) becomes our new width, we reset current width and set the rectangle part to Left.
> instance Rectangly Corner Bar (w, cw, h, TopRight) (cw, Z, h, Left)
The rest is very similar:
> instance Rectangly Corner Dash (w, cw, h, TopLeft) (w, cw, h, Top)
> instance Rectangly Corner Dash (w, cw, h, BottomLeft) (w, w, h, Bottom)
> instance Rectangly Corner End (w, cw, h, BottomRight) (w, cw, h, Bottom)
> instance Rectangly Dash Dash (w, cw, h, Top) (w, (S cw), h, Top)
> instance Rectangly Dash Corner(w, cw, h, Top) (w, (S cw), h, TopRight)
> instance Rectangly Dash Dash (w, (S cw), h, Bottom) (w, cw, h, Bottom)
> instance Rectangly Dash Corner(w, (S Z), h, Bottom) (w, cw, h, BottomRight)
> instance Rectangly Bar Bar (w, cw, h, Left) (w, cw, h, Right)
> instance Rectangly Bar Bar (w, cw, h, Right) (w, cw, (S h), Left)
> instance Rectangly Bar Corner(w, cw, h, Right) (w, cw, (S h), BottomLeft)
Of course, it's not possible to build rectangles with a single combinator (without explicit type sigs everywhere), because the tag of the combinator is polymorphic so there would be an overlap. Binding these three combinators to the r requires specializing the type to the specific tag:
> o :: Rectangly Corner nextTag inpState outState => TagCont Corner inpState (TagCont nextTag outState t -> t)
> o = r
> ᜭ :: Rectangly Dash nextTag inpState outState => TagCont Dash inpState (TagCont nextTag outState t -> t)
> ᜭ = r
> ǀ :: Rectangly Bar nextTag inpState outState => TagCont Bar inpState (TagCont nextTag outState t -> t)
> ǀ = r
All that's left is begin for starting the process and end - the final continuation.
> begin :: TagCont Corner (Z, Z, Z, TopLeft) t -> t
> begin = unTagCont
> data Rectangle w h = Rectangle Int Int deriving Show
> area (Rectangle w h) = w * h
end calculates the rectangle with phantom types set to its Peano dimensions, and corresponding integers at the value level.
> end :: forall w cw h s. (NatToInt w, NatToInt h) => TagCont End (w, cw, h, s) (Rectangle w h)
> end = TagCont $ Rectangle (natToInt (undefined :: w)) (natToInt (undefined :: h))
This is enough to define the following rectangle:
> rectangle = begin
> o ᜭ ᜭ ᜭ ᜭ o
> ǀ ǀ
> ǀ ǀ
> o ᜭ ᜭ ᜭ ᜭ o
> end
The first advantage over the original implementation is the correctness, it's probably a bug, but C++ version doesn't detect the odd number of bars, and what's worse, it calculates them incorrectly in such a case:
unsigned int r1 = ( o-----o
| !
! ! !
! !
o-----o ).area;
unsigned int r2 = ( o-----o
| !
! !
! !
o-----o ).area;
assert (r1 == r2);
Another advantage is what the author calls storing these literals directly in a variable, there's no need to explicitly provide a type, it is inferred automatically:
> r2 = begin
> o ᜭ ᜭ ᜭ o
> ǀ ǀ
> o ᜭ ᜭ ᜭ o
> end
*StaticLiterals> :t r2
r2 :: Rectangle (S (S (S Z))) (S Z)> foo = let r = begin
> o ᜭ ᜭ ᜭ o
> ǀ ǀ
> o ᜭ ᜭ ᜭ o
> end
> in print r
*StaticLiterals> foo
Rectangle 3 1What about errors? They're still impossible, types inferred have contexts that are impossible to fulfill, because there are no such instances. But we can do better! By using Oleg's trick with Fail class we can force ghc to return type errors of our choice.
There's this new paper Errors for the Common Man about debugging type errors, but I don't like it:
- they aren't aware of any solutions to this problem, though they mention HList paper (Fail class trick comes from that paper)
- they talk about generalized state monad, again without mentioning Monadish
- doing research in the area of Haskell type hacks and not being familiar with Oleg's work is a sin
- using state monad to simulate exceptions is bad.
- their idea imposes different type level coding style
- nice error messages require using different api
- no location provided for the errors
Fail class trick solves all of these problems. We provide additional instances to Rectangly class, with a fake Fail dependency with a specially crafted argument. Since Fail doesn't have any instances, it results in a type error, but this error mentions our argument and correct location.
> class Fail x
We need some types for pretty error messages:
> data Expected x y z
> data Either x or z
> data Or
> data ButGot
> data BottomLineToo x
> data Short
> data Long
These instances complement the previous set, trying to make Rectangly a total function, so there will be no errors like "no instance for Rectangly ....", because in these situations, it will match one of these faily instances and reduce to missing Fail instance with a nice error message.
> instance Fail (Expected Dash ButGot tag) =>
> Rectangly Corner tag (w, cw, h, TopLeft) (w', cw', h', s')
> instance Fail (Expected Bar ButGot tag) =>
> Rectangly Corner tag (w, cw, h, TopRight) (w', cw', h', s')
> instance Fail (Expected Dash ButGot tag) =>
> Rectangly Corner tag (w, cw, h, BottomLeft) (w', cw', h', s')
> instance Fail (Expected End ButGot tag) =>
> Rectangly Corner tag (w, cw, h, BottomRight) (w', cw', h', s')
> instance Fail (Expected (Either Dash Or Corner) ButGot tag) =>
> Rectangly Dash tag (w, cw, h, Top) (w', cw', h', s')
> instance Fail (BottomLineToo Short) =>
> Rectangly Dash Corner(w, (S (S n)), h, Bottom) (w', cw', h', s')
> instance Fail (BottomLineToo Long) =>
> Rectangly Dash Corner(w, Z, h, Bottom) (w', cw', h', s')
> instance Fail (Expected (Either Dash Or Corner) ButGot tag) =>
> Rectangly Dash tag (w, cw, h, Bottom) (w', cw', h', s')
> instance Fail (Expected Bar ButGot tag) =>
> Rectangly Bar tag (w, cw, h, Left) (w', cw', h', s')
> instance Fail (Expected (Either Bar Or Corner) ButGot tag) =>
> Rectangly Bar tag (w, cw, h, Right) (w', cw', h', s')
> module StaticLiteralsErrors where
> import StaticLiterals
Let's compare quality of error messages between C++ and Haskell version:
unsigned int r1 = ( o-----o
| -
o-----o ).area;
paczesiowa@laptop /tmp $ g++ tutorial.cpp -o tutorial && ./tutorial
tutorial.cpp: In function ‘int main()’:
tutorial.cpp:34: error: no match for ‘operator-’ in ‘-analog_literals::operator--((analog_literals::
line_end)0u, 0).analog_literals::dashes::operator-- [with T = analog_literals::line_end, unsig
ned int n = 1u](0)’
analogliterals.hpp:72: note: candidates are: analog_literals::line<0u> analog_literals::operator-(an
alog_literals::line_end, analog_literals::line_end) > r1 = area $ begin
> o ᜭ ᜭ o
> ǀ ᜭ
> o ᜭ ᜭ o
> end
No instance for (Fail (Expected Bar ButGot Dash))
arising from a use of `ǀ'
at /home/paczesiowa/blog/04-literals/StaticLiteralsErrors.lhs:23:16
Possible fix:
add an instance declaration for (Fail (Expected Bar ButGot Dash))
In the fifth argument of `begin', namely `ǀ'
In the second argument of `($)', namely
`begin o ᜭ ᜭ o ǀ ᜭ o ᜭ ᜭ o end'
In the expression: area $ begin o ᜭ ᜭ o ǀ ᜭ o ᜭ ᜭ o endError message with the reason can be easily spotted, there is a location (with a column number!) provided, and even number of the wrong combinator ("fifth argument of begin"), shifted one to the left, though. That fix hint doesn't seem very helpful, but I'm sure that throwing an ascii-art of Clippy there would help a lot.
Another example:
unsigned int r1 = ( o-----o
| !
o---o ).area;
tutorial.cpp: In function ‘int main()’:
tutorial.cpp:34: error: no match for ‘operator|’ in ‘analog_literals::operator-
[with unsigned int x
= 2u]((analog_literals::operator--((analog_literals::line_end)0u, 0).
analog_literals::dashes<T, n>:
:operator-- [with T = analog_literals::line_end, unsigned int n = 1u](0),
analog_literals::dashes<an
alog_literals::line_end, 2u>()), (analog_literals::line_end)0u) |
analog_literals::operator- [with u
nsigned int excl_marks = 1u, unsigned int x = 1u]((((analog_literals::
excls<analog_literals::dashes<
analog_literals::line_end, 1u>, 0u>*)(& analog_literals::operator--((
analog_literals::line_end)0u, 0
)))->analog_literals::excls<T, n>::operator! [with T =
analog_literals::dashes<analog_literals::line
_end, 1u>, unsigned int n = 0u](), analog_literals::excls<analog_literals::
dashes<analog_literals::l
ine_end, 1u>, 1u>()), (analog_literals::line_end)0u)’> r2 = area $ begin
> o ᜭ ᜭ o
> ǀ ǀ
> o ᜭ o
> end
No instance for (Fail (BottomLineToo Short))
arising from a use of `ᜭ'
at /home/paczesiowa/blog/04-literals/StaticLiteralsErrors.lhs:61:18
Possible fix:
add an instance declaration for (Fail (BottomLineToo Short))
In the 8th argument of `begin', namely `ᜭ'That's it, the code is available here. Thanks for reading, comments are welcome.
