This file contains hidden or 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
import SwiftUI | |
import PlaygroundSupport | |
struct Foo : View { | |
var body: some View { | |
Circle() | |
.fill(.green) | |
.frame(width: 200, height: 200, alignment: .center) | |
} |
This file contains hidden or 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
* Les: Getting more comfortable with HoTT - Talk: "Bluffers Guide to HoTT" | |
History - Barber's Paradoxes, etc. | |
Russell stratifying set theory | |
Martin Löf in the 1970s | |
In TT - Say term x is of type t -> `x : t` | |
This is a judgement | |
Curry howard - Types and terms = Conjecture/proposition and Proof | |
Things become interesting in the presence of equality | |
equality is always with respect to some type | |
exists t -> x:t = y:t |
This file contains hidden or 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 ScopedTypeVariables #-} | |
{-# LANGUAGE BlockArguments #-} | |
{-# LANGUAGE OverloadedStrings #-} | |
{-# LANGUAGE TypeApplications #-} | |
-- | Small demonstration of GraphQL subscriptions over websockets as per https://github.com/apollographql | |
-- | |
-- * Intended to be a convention over configuration approach. | |
-- * Retries subscription on failures. | |
-- * Provides callbacks for success and errors. |
This file contains hidden or 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 InstanceSigs #-} | |
{-# LANGUAGE RankNTypes #-} | |
{-# LANGUAGE DeriveFunctor #-} | |
{-# LANGUAGE ApplicativeDo #-} | |
{-# LANGUAGE BlockArguments #-} | |
{-# LANGUAGE TypeApplications #-} | |
import Control.Applicative | |
import Control.Exception | |
import Control.Monad |
This file contains hidden or 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 FunctionalDependencies #-} | |
{-# LANGUAGE MultiParamTypeClasses #-} | |
{-# LANGUAGE UndecidableInstances #-} | |
{-# LANGUAGE FlexibleInstances #-} | |
{-# LANGUAGE FlexibleContexts #-} | |
{-# LANGUAGE GADTs #-} | |
-- Wrong! |
This file contains hidden or 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 DeriveFunctor #-} | |
module Main where | |
-- see https://jtobin.io/sorting-with-style | |
import Control.Arrow ((***)) | |
import Data.Function ((&)) |
This file contains hidden or 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 DeriveFunctor #-} | |
module Main where | |
-- see https://jtobin.io/sorting-with-style | |
import Control.Arrow ((***)) | |
import Data.Function ((&)) |
This file contains hidden or 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 BlockArguments #-} | |
module Main where | |
import System.Environment | |
import Control.Monad | |
import Control.Concurrent | |
import Control.Exception.Base | |
{- Inspiration: |
This file contains hidden or 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 TupleSections #-} | |
{-# LANGUAGE FlexibleInstances #-} | |
-- See also: https://github.com/sordina/non-orthogonal-kd-trees#non-orthogonal-kd-trees | |
module Main where | |
import Graphics.Gloss | |
import Graphics.Gloss.Raster.Field | |
import System.Random |
This file contains hidden or 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 OverloadedStrings #-} | |
{-# LANGUAGE BlockArguments #-} | |
{-# LANGUAGE LambdaCase #-} | |
module Main where | |
import Data.AttoLisp | |
import Data.Graph.Inductive.Graph | |
import Data.Graph.Inductive.PatriciaTree | |
import Data.GraphViz |
NewerOlder