JakobBruenker

{-# LANGUAGE BlockArguments #-}
{-# LANGUAGE LambdaCase #-}

module Filter where

import Data.Profunctor
import Data.Profunctor.Product
import Prelude hiding (filter)
import Control.Applicative

JakobBruenker

/*
Constructive proof of Roger's fixed-point theorem in Javascript
===============================================================

N.B. You can load this file in node.js using `.load roger.js` to use the
functions defined here in a REPL.

Definition (Program)
--------------------
Below, a "program" will always be a Javascript function of one argument.

JakobBruenker

Path Visualization

As example, we're using the proof that there's a path between homotopy1 and homotopy2 from Exercise 4.

Instead of looking at a circle, let's look at a general path $p$ between some points $x, y : A$, just because it makes it less confusing to visualize. We'll come back to using the circle later on.

A path is a continuous function of type $[0, 1] \rightarrow A$. If we say $x$ is blue and $y$ is red, we can visualize the path $p$ as a colored image of the interval:

JakobBruenker

{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE MonadComprehensions #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE DeriveDataTypeable #-}

import Data.Data
import Data.Foldable
import Data.Functor
import Data.Maybe

JakobBruenker

data WindowSize = MkWindowSize { windowWidth  :: !Natural
                               , windowHeight :: !Natural
                               }
makeRioClassy ''WindowSize
-- This will generate
-- class (HasWindowWidth env, HasWindowHeight env)
--    => HasWindowSize env where windowSizeL :: Lens' env WindowSize
-- class HasWindowWidth env where ... (method signatures omitted for brevity from here on out)
-- class HasWindowHeight env
-- (as well as associated `id` instances, omitted for brevity for this and the other types)

JakobBruenker

-- Inspired by https://github.com/goldfirere/video-resources/blob/main/2021-07-06-zipWith/ZipWith.hs

{-# LANGUAGE StandaloneKindSignatures, DataKinds, TypeOperators,
             TypeFamilies, UndecidableInstances, GADTs, ScopedTypeVariables,
             TypeApplications, FlexibleInstances, FlexibleContexts,
             ConstraintKinds, FunctionalDependencies, AllowAmbiguousTypes #-}

module Lift where

import Data.Kind

JakobBruenker

{-# LANGUAGE ScopedTypeVariables
           , ViewPatterns
           , LambdaCase
           , BlockArguments
           , StandaloneKindSignatures
           , GADTs
           , TypeOperators
           , ImportQualifiedPost
           , UndecidableInstances
           , DerivingVia

JakobBruenker

{-# LANGUAGE NumDecimals, BlockArguments #-}

import System.Environment
import Data.List

f 0 = (length .) . filter
f 1 = count
f 2 = count' 
f 3 = count''

JakobBruenker

{-# LANGUAGE GADTs, TypeFamilies, DataKinds, TypeOperators, StandaloneDeriving #-}

module Dependent where

data Nat = Z | S Nat

data Vec (n :: Nat) a where
  Nil :: Vec Z a
  Cons :: a -> Vec n a -> Vec (S n) a

JakobBruenker

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

import Data.Kind
import Data.Type.Equality

data Nat = Z | S Nat

data SNat :: Nat -> Type where
  SZ :: SNat Z
  SS :: SNat n -> SNat (S n)