cdepillabout

AR=ar
AR_FOR_TARGET=ar
AS=as
AS_FOR_TARGET=as
CC=gcc
CC_FOR_TARGET=gcc
CONFIG_SHELL=/nix/store/r47p5pzx52m3n34vdgqpk5rvqgm0m24m-bash-4.4-p23/bin/bash
CXX=g++
CXX_FOR_TARGET=g++
DISPLAY=localhost:10.0

cdepillabout

'--cc=/nix/store/10yq7kwlvbc6h658izmrlsspry1g9f3c-gcc-wrapper-7.3.0/bin/cc'
'--cflag=-D__GLASGOW_HASKELL__=804'
'--cflag=-Dlinux_BUILD_OS=1'
'--cflag=-Dlinux_HOST_OS=1'
'--cflag=-Dx86_64_BUILD_ARCH=1'
'--cflag=-Dx86_64_HOST_ARCH=1'
'--cflag=-I.stack-work/dist/x86_64-linux-nix/Cabal-2.2.0.1/build/autogen'
'--cflag=-I.stack-work/dist/x86_64-linux-nix/Cabal-2.2.0.1/build/global-autogen'
'--cflag=-I/home/illabout/.stack/snapshots/x86_64-linux-nix/lts-12.13/8.4.3/lib/x86_64-linux-ghc-8.4.3/network-2.6.3.6-2g6VId0Xlc85XRtUcfQj0T/include'
'--cflag=-I/home/illabout/.stack/snapshots/x86_64-linux-nix/lts-12.13/8.4.3/lib/x86_64-linux-ghc-8.4.3/primitive-0.6.3.0-DaZpcxwJp2TGn8ITSgfI4C/include'

cdepillabout

{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE DefaultSignatures #-}
{-# LANGUAGE DeriveFunctor #-}
{-# LANGUAGE DerivingStrategies #-}
{-# LANGUAGE EmptyCase #-}
{-# LANGUAGE ExistentialQuantification #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}

cdepillabout

let
  nixpkgsTarball = builtins.fetchTarball {
    name = "nixos-unstable-2018-11-09";
    url = https://github.com/nixos/nixpkgs/archive/1c49226176d248129c795f4a654cfa9d434889ae.tar.gz;
    sha256 = "0v8vp38lh6hqazfwxhngr5j96m4cmnk1006kh5shx0ifsphdip62";
  };

  nixpkgs = import nixpkgsTarball { };
in

cdepillabout

I was reading through Type Theory and Formal Proofs (recommended by @parsonsmatt), and there was some info about how to represent "exists" (Ǝ).

In the type-theory version of classical logic, "exists" can represented as a higher-order function using "forall" like the following:

Ǝ x : S. P x is defined as ∀ A : *. (∀ x : S. P x -> A) -> A

cdepillabout

{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
{-# LANGUAGE InstanceSigs #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE PolyKinds #-}

cdepillabout

{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE TypeApplications #-}

-- | This module shows how it is possible to run a function with a constraint of
-- an instance that doesn't exist.
--
-- For instance, in the 'f' function, the 'Lala' 'Int' instance doesn't exist,

cdepillabout

{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE TypeApplications #-}

-- | This modules shows how it is possible to override the functions that get
-- called for a typeclass.
--
-- For instance, the 'foo' function overrides the '(<>)' function for

cdepillabout

Here are some notes for playing around with login-with locally.

login-with assumes that it will be accessed over https. Since we are just playing around with it, we want to run it locally. We don't want to mess with setting up nginx as a reverse proxy.

We can use socat as a quick reverse proxy.

First, we need to create a certificate socat can use. (Ideally, socat would create a certificate for us every time it runs, but it doesn't look like that functionality exists...) openssl is used to create the ceritificate:

$ openssl req -new -x509 -days 365 -nodes -out cert.pem -keyout cert.key

cdepillabout

{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
{-# LANGUAGE InstanceSigs #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE PolyKinds #-}