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

{-# 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 DataKinds #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
{-# LANGUAGE InstanceSigs #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE PolyKinds #-}

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

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

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

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

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

these derivations will be built:
  /nix/store/x5bvnh074wh774yd3n73zgylicjxf408-gi-gdk-3.0.16.drv
  /nix/store/8smaas6jq95knzqbw6inlfhlw97bla0y-gi-gtk-3.0.25.drv
  /nix/store/4a8avkmjxv5sb30qzcshshlx92pwwww0-gi-vte-2.91.19.drv
  /nix/store/912iwrga7jvxn3vawab29hmnfsrpsv3z-termonad-1.0.0.0.drv
  /nix/store/br77czswyk786k0ak8j4hwradp2xxbxw-ghc-8.4.4-with-packages.drv
  /nix/store/g8gags5q5hiiqpzxx45y1kwzf0xkvmf9-termonad-with-packages-8.4.4.drv
building '/nix/store/x5bvnh074wh774yd3n73zgylicjxf408-gi-gdk-3.0.16.drv'...
setupCompilerEnvironmentPhase
Build with /nix/store/dxljd69cp3m5cgfl53h0fjbq202m0fm7-ghc-8.4.4.