EncodePanda

Since macOS Catalina, the root drive is read-only. The solution is to create a separate APFS volume and a “synthetic” /nix directory which points to it:

# Check if /nix exists, if not:
echo 'nix' | sudo tee -a /etc/synthetic.conf
# this will create a "synthetic" empty directory /nix

# REBOOT so macOS sees the synthetic directory

# After rebooting, create an APFS volume for Nix

copumpkin

{-# LANGUAGE GADTs, RankNTypes, TypeFamilies, DataKinds, PolyKinds, TypeOperators, ScopedTypeVariables #-}

-- Lots of ways you can phrase this, but this works for me
-- For folks who haven't seen it before, this is "the essence of the sum type" and sigma stands for sum.
-- You see it far more often in dependent types than elsewhere because it becomes a lot more pleasant to
-- work with there, but it's doable in other contexts too. Think of the first parameter to the data
-- constructor as a generalized "tag" as we talk about in "tagged union", and the second parameter is the
-- "payload". It turns out that you can represent any simple sum type you could write in Haskell this way
-- by using a finite and enumerable `f`, but things can get more unusual when `f` isn't either. In such
-- cases, it's often easier to think of this as the essence of existential types.

nadavrot

High-Performance Matrix Multiplication

This is a short post that explains how to write a high-performance matrix multiplication program on modern processors. In this tutorial I will use a single core of the Skylake-client CPU with AVX2, but the principles in this post also apply to other processors with different instruction sets (such as AVX512).

Intro

Matrix multiplication is a mathematical operation that defines the product of

evancz

A vision for data interchange in Elm

How do you send information between clients and servers? What format should that information be in? What happens when the server changes the format, but the client has not been updated yet? What happens when the server changes the format, but the database cannot be updated?

These are difficult questions. It is not just about picking a format, but rather picking a format that can evolve as your application evolves.

Literature Review

By now there are many approaches to communicating between client and server. These approaches tend to be known within specific companies and language communities, but the techniques do not cross borders. I will outline JSON, ProtoBuf, and GraphQL here so we can learn from them all.

tfausak

# https://mail.haskell.org/pipermail/ghc-devs/2017-July/014364.html
# https://downloads.haskell.org/~ghc/8.2.1-rc3/
# http://taylor.fausak.me/2017/05/17/testing-ghc-release-candidates-with-stack/
compiler: ghc-8.2.0.20170704
compiler-check: match-exact

resolver: ghc-8.2.0.20170704

setup-info:
  ghc:

goldfirere

{-# LANGUAGE TemplateHaskell, ScopedTypeVariables, TypeInType, TypeOperators,
             TypeFamilies, GADTs, UndecidableInstances, InstanceSigs #-}
{-# OPTIONS_GHC -Wincomplete-patterns #-}

import Data.Kind
import Data.Singletons.TH
import Data.Singletons.Prelude
import Prelude hiding ( take )

$(singletons [d|

klaftertief

• Star this gist to see the talk at ReactiveConf 2016.
• Retweet to spread the word.
• Have a look at this blog post to see other proposals.
• Try elm-search to see what this is all about.

---

An API search engine in Elm for Elm

Elm is a statically typed functional language that compiles to JavaScript. It's well-known for its developer experience: the compiler provides nice error messages, the package system enforces semantic versioning for all published packages and makes sure every exposed value or type has some documentation and type annotations.

AndrasKovacs

{-# language DataKinds, PolyKinds, ScopedTypeVariables, UndecidableInstances,
    FlexibleInstances, FlexibleContexts, GADTs, TypeFamilies, RankNTypes,
    LambdaCase, TypeOperators, ConstraintKinds #-}

import GHC.TypeLits
import Data.Proxy
import Data.Singletons.Prelude
import Data.Singletons.Decide
import Data.Constraint

david-christiansen

module NatInd

import Language.Reflection.Elab
import Language.Reflection.Utils

%default total

trivial : Elab ()
trivial = do compute
             g <- snd <$> getGoal

david-christiansen

module Finite

import Data.Fin
import Language.Reflection.Elab
import Language.Reflection.Utils

%default total

||| A bijection between some type and bounded numbers
data Finite : Type -> Nat -> Type where