External Content not shown. Further Information.

Popular Culture:

• Patrick Stewart kontert EU-Gegner mit Monty-Python-Persiflage
• Ostrich hit by car after activists 'free' it from circus
• Keine barrierefreien Bücher für blinde und sehbehinderte Menschen

Nerd Culture:

• Fake Windows Updates
• The case for base twelve
• Drone-Mounted Chainsaw

Science, Software, Hardware:

• Deinstallation von Apples Quicktime führt zu Problemen bei Adobe-Software – bei Adobe fragt man sich manchmal…
• New State of Water Molecule Discovered
• I am unwilling to relocate again (and it will probably cost me my academic “career”)
• Nanoparticle acts like Trojan horse to halt asthma

Zeroth World:

• 6 Horrifying Realities Of Dealing With Sandy Hook 'Truthers' – this is so absurd.
• Buzz Aldrin punches Bart Sibrel after being harassed by him – also absurd.

Comics/Images/Audios/Videos/Games/Art:

• Child Labour
• If the Flying Spaghetti Monster didn't create life…
• What depression feels like
• The Mess
• Musician

Quotes:

• Some people are like slinkies… …not really good for much but bring a smile to your face when pushed down the stairs.

External Content not shown. Further Information.

Popular Culture:

• Liebe Fleischesser, wollt ihr mal sehen auf welch intelligente Weise man euer Essen tötet?
• Man fishes for lost key, pulls out hand grenade instead

Nerd Culture:

• Will You Be Able to Pick Link's Gender What if Zelda was a Girl
• Die Wassermelone, die das Internet verrückt macht

Science, Software, Hardware:

• Openworm – Fluid dynamics engine is published!

Zeroth World:

• Internet Mapping Glitch Turned a Random Kansas Farm into a Digital Hell

Comics/Images/Audios/Videos/Games/Art:

• They grow up so fast
• Job Security
• Nothing
• Life is great
• The Chug Rag
• Darkness
• Drugs

External Content not shown. Further Information.

Popular Culture:

• Individuelles Trinkbedürfnis – Wenn er ca. 3,5 Liter pro Tag trinkt, muss die Krankenkasse dem Mann auch medizinische Hilfsmittel in diesem Umfang bewilligen. Dies hat das Sozialgericht Dresden entschieden. – i can't even.
• Was Menschen mit Behinderung durch die AfD droht

Nerd Culture:

• 5 Future Things That Have Already Happened

Science, Software, Hardware:

• Notty (via)
• Dank neuer Nasenklammer nie wieder vom Schnarchen gestört werden
• Ubuntu läuft nativ in Windows 10 – naja, ich bin da eher skeptisch, wenn ich bedenke, wie oft M$ schon versucht hat, unixoide Systeme zu unterstützen. Aber könnte klappen.
• UbuntuBSD beta releas – find ich da deutlich interessanter.
• Russland will mit Atomenergie zum Mars – und wieder zurück
• On the Madness of Optimizing Compilers
• Frequently rediscovered technologies
• WinToHDD: install Windows without DVD or USB
• ThinkPenguin VPN mini-router now FSF-certified to respect your freedom

Zeroth World:

• Internet-Connected Rectal Thermometer
• Uploading the Mind to a Computer – "Within the next 30 years, I am going to make sure that we can all live forever." promises Dmitry Itskov.
• Scientists Propose Biodiversity Lab to Redeem Guantanamo Prison Camp
• Nach Autounfall: NPD-Chef lobt Flüchtlinge

Comics/Images/Audios/Videos/Games/Art:

• Left Arm
• Prank
• One More Lap
• War On Drugs
• Miracle Chip
• Good Intentions
• Saint Schrödinger
• Paperwork
• Tapestry Triforce (via)
• Adaptations
• End All Wars
• Ants
• Do You Work Here?
• Can you fold paper more than 7 times with hydraulic press
• Spoiled Children
• Modern-Day Moses
• Universal Install Script
• Earthling
• Slightly NSFW: Autostereogram
• Another Autostereogramm
• Girlfriend
• No Lives Matter

Quotes:

• Reality TV
• Cereal
• I will bathe you…
• Dumm
• The best part about getting vaccinated
• Give a man a fish
• Same sex marriage
• Black People
• There are more airplanes in the sea… …than there are submarines in the sky

External Content not shown. Further Information.

After a long ride on German trails I kindly want to make the request to the programmers of the messenger.com web app to please die in a chemical fire.

Then, Facebook could maybe pay some student to hack together a simple interface that just does - say - autorefresh every few seconds.

Well, admittedly, ping times of 21686ms, which are common in Germany, are a problem when programming certain kinds of low latency network software. I wouldn't blame, for example, MineCraft to not work under these conditions.

But a simple text chat – and yes, that's what your "web app" is – should work perfectly well under that conditions.

And yes, I tried your Android app, and it is even worse. It drains my battery, has the same issues, and above that, I had situations where the messages were not synced correctly (or at all) between my devices.

And don't tell me that this was too hard to implement. Skype has a similar messaging website. And it works perfectly. Even WhatsApp Web works better, though it is annoying that they want an active connection with the phone.

Now after a long pause, a little link list. Sorry, I really don't have much time to keep the blog up right now.

Popular Culture:

• So viele Hürden lauern auf Studierende mit Behinderung
• Smartphones nicht unters Kopfkissen legen

Nerd Culture:

• Sitzkoffer.de ~ falls mal jemand nach nem Geschenk für mich sucht xP
• Long Now Foundation
• The story behind Islamic Rage Guy
• Neue Star-Trek-TV-Serie wird nicht die Star-Trek-Mythologie nutzen

Science, Software, Hardware:

• Khronos Group Releases Vulkan 1.0 Graphics Specification
• Video: The Banach–Tarski Paradox (via)
• Video: Messages For The Future
• 520-Million-Year-Old Nervous System Discovered
• Gene Therapy Human Trial Will Inject Virus Into the Retinas of the Legally Blind
• Parallel OpenGL FAQ

Zeroth World:

• "SKYNET" Might Have Killed Thousands of Innocent People - in Real Life
• Digital Preservation Management
• IBM arbeitet an Software, die Flüchtlinge von Terroristen unterscheiden soll

Comics/Images/Audios/Videos/Games/Art:

• Who Is There?
• Impostor
• Motivation
• Autism Causes Vaccines
• The good life
• Mammoth
• Mafia
• Not this time, son
• Flashing Lights
• TV Chef
• Vaccines Work
• Wishing Well
• Honest

Quotes:

• What do you get when you cross a cow with an octopus? a visit from the ethics committee and immediate withdrawal of your funding
• Fun fact: If humans stood in a single file line around the equator… most of them would drown.
• We vandalize things that aren't ours… …whith qoutes we didn't write to impress people taking shits.

External Content not shown. Further Information.

As I always forget them, here a short list of functions regarding several sum- and product types in Coq. If I missed something, feel free to send me a comment.

Product types:

notation    | name     | left proj. | right proj. |
------------+----------+------------+-------------+
A /\ B      | and      | proj1      | proj2       |
A * B       | pair     | fst        | snd         |
{x | A}     | exist    | proj1_sig  | proj2_sig   |
{x : B & A} | existT   | projT1     | projT2      |

Sum Types:

notation    | name     | intro left | intro right |
------------+----------+------------+-------------+
A \/ B      | or       | or_introl  | or_intror   |
A + B       | sum      | inl        | inr         |
{A} + {B}   | sumbool  | left       | right       |

Scheiß Technik.

Popular Culture:

• Volkswagen sold more sausages than cars in 2015
• Kindesmissbrauch durch Whats-App-Nachricht – Begriffsinflation.

Nerd Culture:

• Calculator Built In Super Mario Level.

Science, Software, Hardware:

• Your Text Editor Is Malware
• Multi-process Firefox’s will use up to 20% more RAM initially
• ZFS is Coming to Ubuntu LTS 16.04
• Homeopathy Effective for Zero Out of 68 Illnesses. – what a surprise.
• Schwimmen bis zur Verzweiflung
• Damascus steel – ancient nanotechnology.
• So sollen blinde Menschen ihr Augenlicht zurückgewinnen – naja, zumindest Leute mit Retinitis Pigmentosa.
• bat-country – an extendible, lightweight Python package for deep dreaming with Caffe and Convolutional Neural Networks.
• Intels Skylake-Prozessoren sind fehlerhaft
• Cotton candy machines help create artificial organs
• Other single-file public-domain/open source libraries with minimal dependencies

Zeroth World:

• Vögel als Brandstifter entlarvt – wieso sollen auch immer nur Menschen die Umwelt zerstören‽

Comics/Images/Audios/Videos/Games/Art:

• Anti-Feminist Barbie
• GENius
• Der Merkel-Obama-Song – so kann Schlager schön sein :3
• Computer Problems
• Java
• The Bachelor
• Time Machine

Quotes:

• Wenn ihr euch mal wieder alleine fühlt…

Hi. There are currently some problems with my markdown setup. I am also refactoring some parts of this website. Behold! #technikeristinformiert

Update: Ok. Most of the problems should be solved now. One problem is that cl-markdown and the original Markdown have slightly different opinions about when a list begins. So some older link lists are still scrambled.

The good news is that most MathJax is gone in favor of svg-latex, which loads a lot faster (though it does not look quite so good).

If you see otherwise scrambled pages, feel free to drop a comment or mail about it. At the moment, I do not have the time to go through every single post I made.

External Content not shown. Further Information.

Arrays in Haskell can be a pain. Monads are a nice thing, but for some things, I would prefer linear types. There are so-called DiffArrays in Haskell, which are, for no apparent reason, ridiculously slow.

As a quick reminder: A DiffArray maintains a history of changes, which should be only linear overhead and when using it linearly only, most of the memory overhead should be quite short-lived. But it isn't.

My idea now is different: Using an array only linearly should be trivial to check when having an AST (and I wonder why nobody has written such a thing yet which just replaces linearily used DiffArrays with unsafe operations). But other than overwriting the old array with a difference, I just mark it as invalid:

import System.IO.Unsafe
import Data.IORef
import Data.Array.IO

data LinearArray_ = Invalid | Valid (IOUArray Int Int)
type LinearArray = IORef LinearArray_

Creating new Arrays is straightforward:

newArray :: (Int, Int) -> Int -> LinearArray
newArray (start, end) init =
    unsafePerformIO $
    do
      t <- Data.Array.IO.newArray (start, end) init
      r <- newIORef (Valid t)
      return $ r

Overwriting an array does the following: It takes the array from the old ref and overwrites it accordingly. Then the old ref is overwritten and marked Invalid, and a new array is returned. Of course, if the old ref was Invalid already, an error is rised:

overwriteArray :: LinearArray -> Int -> Int -> LinearArray
overwriteArray old index value =
    unsafePerformIO $
    do ior <- readIORef old
       case ior of
         Invalid -> error "nonlinear use of linear array!"
         Valid a -> do
                  writeArray a index value
                  writeIORef old Invalid
                  new <- newIORef (Valid a)
                  return new

Trying to read from an invalid array will do the same:

readArray :: LinearArray -> Int -> Int
readArray arr index =
    unsafePerformIO $
    do ior <- readIORef arr
       case ior of
         Invalid -> error "nonlinear use of linear array!"
         Valid a -> do
                  r <- Data.Array.IO.readArray a index
                  return r

This approach has several caveeats. For example, in most functional languages, one can just overload a name. In Haskell, a code like

let {a = []} in let {a = 1 : a} in a

produces an infinite list of ones: By default, a refers to itself, and all definitions are recursive. But name overloading is something that comes in handy when using linear arrays. Another caveeat is lazy evaluation. The following code "surprisingly" works:

a :: Int
a = let arr1 = Main.newArray (0, 10) 0
        arr2 = overwriteArray arr1 9 1
    in Main.readArray arr1 9

That is because arr2 is never evaluated. However, activating {-# LANGUAGE BangPatterns #-} and using

a :: Int
a = let arr1 = Main.newArray (0, 10) 0
        !arr2 = overwriteArray arr1 9 1
    in Main.readArray arr1 9

will throw an error. Notice that both are wrong, in the sense that the specification of a linear array requires linear occurences only, but arr1 occurs twice. It is only that there is no error in the one case.

My benchmarks show that this kind of array is pretty fast. Now, while feeling a lynchmob of Haskell-fanboys forming, let me add that I would not recommend to actually use this. I would just wish that Haskell had support for uniqueness types – or at least automatic optimization of linearly used immutable arrays or DiffArrays in that manner.

Because it should be quite easy to find out whether an array occurs only once in a term, and all its decendants are also only used once. And the benefits would be really huge, in my opinion.