import Data.Functor.Yoneda
import Data.Char
import Data.Kind
infixr 5
·
type List :: (Type -> Type) -> Constraint
class List f where
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
{-# LANGUAGE DataKinds #-} | |
{-# LANGUAGE FlexibleContexts #-} | |
{-# LANGUAGE FlexibleInstances #-} | |
{-# LANGUAGE FunctionalDependencies #-} | |
{-# LANGUAGE GADTs #-} | |
{-# LANGUAGE KindSignatures #-} | |
{-# LANGUAGE ScopedTypeVariables #-} | |
{-# LANGUAGE TypeApplications #-} | |
{-# LANGUAGE TypeOperators #-} | |
{-# LANGUAGE UndecidableInstances #-} |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
{-# 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 |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
let | |
nixpkgs = import ((import <nixpkgs> { }).fetchFromGitHub { | |
owner = "NixOS"; | |
repo = "nixpkgs"; | |
rev = "72f07e74f3bcac0635b880fecbd45c17938a6368"; | |
sha256 = "081qi4hpxzw3w5kphv1qcxyayh542szdshmacz2kpfj9d04d3nzc"; | |
}) { config = { }; }; | |
in | |
nixpkgs.callPackage ./pinned-ghc.nix {} |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
#!/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 } |
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.
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
{-# language TypeApplications #-} | |
{-# language TypeFamilies #-} | |
{-# language FlexibleInstances #-} | |
{-# language ScopedTypeVariables #-} | |
data Unit = U | |
class C (k :: Unit) where | |
get :: Int |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
{-| | |
- 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. | |
- |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
-- 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 |