i-am-tom

{-# LANGUAGE DataKinds              #-}
{-# LANGUAGE FlexibleContexts       #-}
{-# LANGUAGE FlexibleInstances      #-}
{-# LANGUAGE FunctionalDependencies #-}
{-# LANGUAGE GADTs                  #-}
{-# LANGUAGE KindSignatures         #-}
{-# LANGUAGE ScopedTypeVariables    #-}
{-# LANGUAGE TypeApplications       #-}
{-# LANGUAGE TypeOperators          #-}
{-# LANGUAGE UndecidableInstances   #-}

Icelandjack

import Data.Functor.Yoneda
import Data.Char
import Data.Kind

infixr 5
  ·

type  List :: (Type -> Type) -> Constraint
class List f where

Icelandjack

Non-standard operators I use :) linked to from my twitter profile

I use kind synonyms

type T   = Type
type TT  = T -> T
type TTT = T -> TT
type C   = Constraint
type TC  = T -> C

Lysxia

{-# LANGUAGE TypeFamilies, UndecidableInstances #-}

-- https://blog.poisson.chat/posts/2018-07-09-type-gadt.html

module UnMTL where

import Control.Monad.Trans.Reader
import Control.Monad.Trans.State
import Control.Monad.Trans.Except
import Data.Functor.Identity

mpickering

let
  nixpkgs = import ((import <nixpkgs> { }).fetchFromGitHub {
  owner = "NixOS";
  repo = "nixpkgs";
  rev = "72f07e74f3bcac0635b880fecbd45c17938a6368";
  sha256 = "081qi4hpxzw3w5kphv1qcxyayh542szdshmacz2kpfj9d04d3nzc";
}) { config = { }; };
in
  nixpkgs.callPackage ./pinned-ghc.nix {}

jship

#!/usr/bin/env stack
-- stack --resolver lts-10.8 --install-ghc exec ghci

{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE ExistentialQuantification #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE LambdaCase #-}

-- A key type for pretend use in looking up a doggo in a database.
newtype Key a = Key { unKey :: String }

AndyShiue

I think I’ve figured out most parts of the cubical type theory papers; I’m going to take a shot to explain it informally in the format of Q&As. I prefer using syntax or terminologies that fit better rather than the more standard ones.

Q: What is cubical type theory?

A: It’s a type theory giving homotopy type theory its computational meaning.

Q: What is homotopy type theory then?

A: It’s traditional type theory (which refers to Martin-Löf type theory in this Q&A) augmented with higher inductive types and the univalence axiom.

lukaszlew

{-# language TypeApplications #-}
{-# language TypeFamilies #-}
{-# language FlexibleInstances #-}
{-# language ScopedTypeVariables #-}

data Unit = U

class C (k :: Unit) where
  get :: Int

gatlin

{-|
 - Example of using free constructions to build a flexible little compiler.
 -
 - The goal here is not necessarily efficiency but readability and flexibility.
 -
 - The language grammar is represented by an ADT; however, instead of
 - recursively referring to itself it instead references a type variable.
 -
 - We derive instances of 'Functor' and 'Traversable' for this type.
 -

tfausak

-- stack --resolver lts-10.0 script
{-# LANGUAGE DeriveGeneric #-}
{-# LANGUAGE FlexibleContexts #-}
import qualified Data.Aeson as Json
import Data.Aeson.Encode.Pretty (encodePretty)
import Data.ByteString (ByteString)
import Data.ByteString.Lazy (writeFile)
import Data.Colour.SRGB (sRGB24)
import qualified Data.CSV.Conduit as Csv
import qualified Data.CSV.Conduit.Conversion as Csv