gylterud

5 ms·

31.
by gylterud 1y ago
The above just test for existence, but a slight modification, based on the same logical expression, gets us to a winning strategy: -- Game data data Player = P1 | P2 deriving (Eq, Show) data Color = Red | Blue
32.
by gylterud 1y ago
Yes, but the connection is not clear from what I wrote. I keep intending to make a little post about the connection, but I want it to highlight some Haskell code I wrote, but I haven't polished it yet. I want to make an update to it, u
33.
by gylterud 1y ago
This is the idea behind Kolmogorov complexity[0], that the complexity of a string (finite or infinite) can be measured, relative to a programming language, as the the length of shortest program which produces it. Precisely computing the Kol
34.
by gylterud 1y ago
Should be fixed now! I hope the writing is easier to bare now.
35.
by gylterud 1y ago
That's a neat thought! One could interpret the outcome of the game as a number by ○ being the digit 0 and ● being 1. For fun we could also say that if there is a repeating subsequence at the end (someone lost), then that is repeated in
36.
by gylterud 1y ago
If it was a file filled entirely with one character, the compression could simply be to write a file saying "this character copied 3 million times", which is less than 512 bytes. This is not exactly what happens here, but many com
37.
Logic and Creativity(hakon.gylterud.net)
2 points by gylterud 1y ago|1 comments
38.
by gylterud 1y ago
This is a text I wrote a few years ago about the false dichotomy between logic and creativity. But with the advent of LLMs I thought about again. I think current LLMs are capable of both logic and creativity, but still to a limited extent.
39.
The Anti-Pattern Game(hakon.gylterud.net)
66 points by gylterud 1y ago|48 comments
40.
by gylterud 1y ago
This little game I made might be one of the most tedious little games to actually play. But I found it great fun to analyse! (For the initiated, I should mention that it is related to Thue–Morse sequences.)
41.
by gylterud 1y ago
Seems fixes now!
42.
by gylterud 1y ago
Knew I would find it here, unless it was a me problem. Both web and iOS app are just showing me empty lines instead of emails. Fingers crossed it will be fixed really soon.
43.
by gylterud 1y ago
What are you on about? The Agda compiler, Pugs, Cryptol, Idris, Copilot (not that copilot you are thinking of), GHC, PureScript, Elm… These might not be mainstream, but are (or were for Pugs, but the others are current) important within the
44.
by gylterud 1y ago
Yes, but there is very little modern latin slang. While GHC gives us great new extensions of Haskell quite often.
45.
by gylterud 1y ago
There are lots of great libraries, like repa, servant, megaparsec, gloss, yampa… as well as bindings to lots of standard stuff. I consider parsing to be one of Haskell’s killer strengths and I would definitely use it to write a compiler. Th
46.
by gylterud 1y ago
What makes you believe Haskell is dead or even dying? New versions of GHC are coming out, and in my experience, developing Haskell has never been smoother (that’s not to say it is completely smooth).
47.
by gylterud 1y ago
This is one of the reasons I prefer Agda. It is usually written without tactics, you just write the proof term in a functional programming language via the Curry–Howard correspondence. The trade off is that you must be more disciplined with
48.
by gylterud 1y ago
Not downvoting, but any typical online activity during commute or while travelling will blow through 1GB. Music every day, or a video once in a while… I also have WiFi at my usual hangs, but thus far this month I am on 15GB of my 50GB month
49.
by gylterud 1y ago
Not a contradiction to anything you said, but O3 will sometimes whip up a python script to analyse the pictures I give it. For instance, I asked it to compute the symmetry group of a pattern I found on a wallpaper in a Lebanese restaurant t
50.
by gylterud 1y ago
At least on Linux you have 100 choices of window manager (and 100 themes of KDE). 101 if you roll up your sleeves and roll your own.
51.
by gylterud 1y ago
The lecture? No, unfortunately.
52.
by gylterud 1y ago
With Haskell code it is often so that the code which actually does something is expressed in terms of combinators. These combinators are often very general, so one must do a bit of mental work to understand what they do in this particular c
53.
by gylterud 1y ago
Oh, I owe a lot to freenode and #haskell and #math in particular. I remember one of them ran a lecture on category theory, live. It was also there I first heard about Martin-Löf type theory. It was such a great time and place for a young pe
54.
by gylterud 1y ago
Pondering mathematical objects such as BB(n) is exactly the kind of stuff which rooks one’s faith in classical logic.
55.
by gylterud 1y ago
A constructive mathematician would indeed deny that BB(748) is a well defined number. One could define it as a predicate on natural numbers, but lest we find a contradiction in ZFC we cannot hope to constructively prove that it holds for an
56.
by gylterud 1y ago
Like you I have kids, and it really takes a toll, and I definitely see myself aging in the mirror. But I cannot recommend training enough. I started working out regularly three years ago, after a long hiatus due to kids. And I feel stronger
57.
by gylterud 1y ago
U+263A entered Unicode in 1993, afaik. Plan9 had utf8 support in the terminal back then!
58.
by gylterud 1y ago
Reminds me of Plan 9 with its plumber! Especially when combined with Acme, win and right clicking to search backwards.
59.
by gylterud 1y ago
Why? Why would the language used to express proof of correctness have anything to do with English? English was not developed to facilitate exact and formal reasoning. In natural language ambiguity is a feature, in formal languages it is unw
60.
by gylterud 1y ago
I think type theory is exactly right for this! Being so similar to programming languages, it can piggy back on the huge amount of training the LLMs have on source code. I am not sure lean in part is the right language, there might be challe

More ›