ghuntley

👋 Hi, I'm Geoff. I stole off all your NFTs.

I respectfully ask that you don't quote me as “$company person Geoffrey Huntley said” – if I speak for a company, I will publish on its channels. My full name is "Geoffrey Huntley" please use that and not "Geoff Huntley".

• website: https://ghuntley.com/
• newsletter: https://ghuntley.com/newsletter
• twitter: https://www.twitter.com/geoffreyhuntley.com
• linkedin: https://www.linkedin.com/in/geoffreyhuntley

runarorama

Advent of Code 2019, in Unison

Spoilers for Advent of Code 2019 follow.

Day 1: The Tyranny of the Rocket Equation

Fuel required to launch a given module is based on its mass. Specifically, to find the fuel required for a module, take its mass, divide by three, round down, and subtract 2.

This describes a simple function. There seems to be an oversight in the problem statement that modules with very low mass have a negative fuel requirement. I'm going to assume that's not right, and that instead of integer subtraction, we want natural number subtraction (sometimes called "monus"). In Unison, we can use the Nat type instead of integers, so we don't have to consider negatives. The subtraction operation is called drop:

dysinger

# MOVED HERE https://gist.github.com/dysinger/2a768db5b6e3b729ec898d7d4208add3

vaibhavsagar

let
  nixpkgs-src = builtins.fetchTarball {
    url = "https://github.com/NixOS/nixpkgs-channels/archive/f197f57bd336746b53e5f1668ac7df1b63da7c9f.tar.gz";
    sha256 = "0cj4h39fhrm0nzxgfcjxy457zhi2rajpgm6abas816srmr4bb6nn";
  };
  semantic-src = builtins.fetchTarball {
    url = "https://github.com/github/semantic/archive/78dad094fa2380aef36cabd48d57f6122f1034ec.tar.gz";
    sha256 = "0bk7f96fm9928nc2yv85cwchk43xh4yikbiqg7ngba5q6gj7xy04";
  };
  pkgs = import nixpkgs-src { config.allowBroken = true; };

jmoy

section ‹A Simple Graph Problem›

text ‹
We shall prove the following: "In a finite group of people, some of whom are friends with some
of the others there must be at least two people who have the same number of friends."
›

theory Friends
  imports   Main 
            Finite_Set 

porglezomp

import Data.Vect

-- `minus` is saturating subtraction, so this works like we want it to
eq_max : (n, k : Nat) -> maximum k n = plus (n `minus` k) k
eq_max  n     Z    = rewrite minusZeroRight n in rewrite plusZeroRightNeutral n in Refl
eq_max  Z    (S _) = Refl
eq_max (S n) (S k) = rewrite sym $ plusSuccRightSucc (n `minus` k) k in rewrite eq_max n k in Refl

-- The type here says "the result is" padded to (maximum k n), and is padding plus the original
leftPad : (x : a) -> (n : Nat) -> (xs : Vect k a)

xgrommx

{-# LANGUAGE StandaloneDeriving, DataKinds, PolyKinds, GADTs, RankNTypes, TypeOperators, FlexibleContexts, TypeFamilies, KindSignatures #-}

-- http://www.timphilipwilliams.com/posts/2013-01-16-fixing-gadts.html

module HRecursionSchemes where

import Control.Applicative
import Data.Functor.Identity
import Data.Functor.Const
import Text.PrettyPrint.Leijen hiding ((<>))

sellout

-- | A “flushing” 'stream', with an additional coalgebra for flushing the
--   remaining values after the input has been consumed. This also allows us to
--   generalize the output away from lists.
fstream
  :: (Cursive t (XNor a), Cursive u f, Corecursive u f, Traversable f)
  => Coalgebra f b -> (b -> a -> b) -> Coalgebra f b -> b -> t -> u
fstream ψ g ψ' = go
  where
    go c x = 
      let fb = ψ c

kritzcreek

Generating collections of random numbers in PureScript

A problem that I've seen beginners run into in Haskell or PureScript a couple of times now is how to generate a List of random numbers. It's a common requirement for little games (which make for great first projects) to generate these, and it definitely seems to be a stumbling block.

Why are random numbers hard?

Randomness is considered a side effect in purely functional languages, which means that to generate them you usually need access to Eff/IO, which in turn means we need to deal with Monads. And while generating a single random number is usually pretty easy with do-notation, the typical intuition beginners have built when going from single values to a collection is to use map, but that fails.

Type-Directed-Search to the rescue

dbarnes

OSX Sierra + Titan Xp eGPU. Tensorflow 1.2.1. + CUDA 8 + cuDNN 6

This gist summarises the tensorflow related steps I took to get the above combo working.

When its all tested in c++ I'll update the instructions fully (and add anything I forgot below).

But in summary ( with the current master dd06643cf098ed362212ce0f76ee746951466e81 ):

I have uploaded the pip wheel which I believe should work if you have the same setup but no promises (built for compute capability 3.5, 5.2, 6.0 and named tensorflow-gpu). Install with (not sure dropbox allows this direct linking):