this repo has no description
initial commit with first notebook
+317
+3
README.md
+3
README.md
+31
default.nix
+31
default.nix
···
1
+
let
2
+
fetcher = { owner, repo, rev, sha256, ... }: builtins.fetchTarball {
3
+
inherit sha256;
4
+
url = "https://github.com/${owner}/${repo}/archive/${rev}.tar.gz";
5
+
};
6
+
7
+
inherit (import <nixpkgs> {}) lib;
8
+
9
+
versions = lib.mapAttrs
10
+
(_:fetcher)
11
+
(builtins.fromJSON (builtins.readFile ./versions.json));
12
+
13
+
14
+
overlay = self: super: {
15
+
python3 = super.python3.override {
16
+
packageOverrides = p-self: p-super: {
17
+
docutils = p-super.docutils.overridePythonAttrs (old: {doCheck = false;});
18
+
};
19
+
};
20
+
};
21
+
22
+
nixpkgs = import versions.nixpkgs { overlays = [ overlay ]; };
23
+
24
+
in
25
+
import "${versions.ihaskell}/release.nix" {
26
+
inherit nixpkgs;
27
+
compiler = "ghc844";
28
+
packages = self: with self; [
29
+
papa
30
+
];
31
+
}
+244
logical-equivalences-in-haskell.ipynb
+244
logical-equivalences-in-haskell.ipynb
···
1
+
{
2
+
"cells": [
3
+
{
4
+
"cell_type": "markdown",
5
+
"metadata": {},
6
+
"source": [
7
+
"---\n",
8
+
"title: \"Logical equivalences in Haskell\"\n",
9
+
"published: 2019-01-03\n",
10
+
"tags: technology haskell\n",
11
+
"link: \n",
12
+
"---"
13
+
]
14
+
},
15
+
{
16
+
"cell_type": "markdown",
17
+
"metadata": {},
18
+
"source": [
19
+
"\n"
20
+
]
21
+
},
22
+
{
23
+
"cell_type": "markdown",
24
+
"metadata": {},
25
+
"source": [
26
+
"The blogpost [Classical Logic in Haskell](https://cvlad.info/clasical-logic-in-haskell/) established a way to prove equivalences between logical propositions and _law of excluded middle_ by writing intances of `Iso` for the same propositions wrapped in a `newtype`. [Vladimir's](https://twitter.com/cvlad) post contain proofs of some important propositions. I had fun proving them myself. I wanted to continue with some more. \n",
27
+
"\n",
28
+
"Recently, I did the [Logic and Proof](https://leanprover.github.io/logic_and_proof/) course to learn both proof techniques and [Lean](https://leanprover.github.io/) theorem prover. It was fun. So I picked few propositions from the exercises of the [Propositional Logic in Lean](https://leanprover.github.io/logic_and_proof/propositional_logic_in_lean.html#exercises) chapter to try write equivalence proofs for them.\n",
29
+
"\n",
30
+
"Below are the propositions as newtypes (their logical notations mentioned as comment) and subsequently the `Iso` instances to prove their equivalences with `Lem`. As mentioned in the original blogpost, one nice way to progress here is by taking clues from the type system itself in the form of [typed holes](https://wiki.haskell.org/GHC/Typed_holes)."
31
+
]
32
+
},
33
+
{
34
+
"cell_type": "markdown",
35
+
"metadata": {},
36
+
"source": [
37
+
"\n"
38
+
]
39
+
},
40
+
{
41
+
"cell_type": "markdown",
42
+
"metadata": {},
43
+
"source": [
44
+
"Let's set some language pragmas"
45
+
]
46
+
},
47
+
{
48
+
"cell_type": "code",
49
+
"execution_count": 1,
50
+
"metadata": {},
51
+
"outputs": [],
52
+
"source": [
53
+
":set -XMultiParamTypeClasses\n",
54
+
":set -XRankNTypes\n",
55
+
":set -XInstanceSigs\n",
56
+
":set -XScopedTypeVariables\n",
57
+
":set -XTupleSections"
58
+
]
59
+
},
60
+
{
61
+
"cell_type": "markdown",
62
+
"metadata": {},
63
+
"source": [
64
+
"Required `Iso` class from the original blogpost put inside a module so that it can be imported for rest of the sections"
65
+
]
66
+
},
67
+
{
68
+
"cell_type": "code",
69
+
"execution_count": 2,
70
+
"metadata": {},
71
+
"outputs": [],
72
+
"source": [
73
+
"module Proof where\n",
74
+
"import Data.Void (Void, absurd)\n",
75
+
"\n",
76
+
"class Iso a b where\n",
77
+
" to :: a -> b\n",
78
+
" from :: b -> a\n",
79
+
" \n",
80
+
"-- Law of excluded middle\n",
81
+
"-- forall P. P \\/ -P\n",
82
+
"newtype Lem m = \n",
83
+
" Lem\n",
84
+
" (forall a .\n",
85
+
" m (Either a (a -> m Void))) "
86
+
]
87
+
},
88
+
{
89
+
"cell_type": "code",
90
+
"execution_count": 3,
91
+
"metadata": {},
92
+
"outputs": [],
93
+
"source": [
94
+
"import Data.Void\n",
95
+
"import Proof"
96
+
]
97
+
},
98
+
{
99
+
"cell_type": "markdown",
100
+
"metadata": {},
101
+
"source": [
102
+
"\n"
103
+
]
104
+
},
105
+
{
106
+
"cell_type": "markdown",
107
+
"metadata": {},
108
+
"source": [
109
+
"And now the propositions..."
110
+
]
111
+
},
112
+
{
113
+
"cell_type": "code",
114
+
"execution_count": 4,
115
+
"metadata": {},
116
+
"outputs": [],
117
+
"source": [
118
+
"-- forall. P,Q. P /\\ (P -> Q) -> Q\n",
119
+
"\n",
120
+
"import Control.Monad.Fix\n",
121
+
"\n",
122
+
"newtype Prop1 m = \n",
123
+
" Prop1 \n",
124
+
" (forall a b. \n",
125
+
" (a , (a -> m b)) -> m b)\n",
126
+
" \n",
127
+
"-- proof, implication elimination <==> LEM\n",
128
+
"instance Monad m => Proof.Iso (Prop1 m) (Lem m) where\n",
129
+
" from :: Lem m -> Prop1 m\n",
130
+
" from _ = Prop1 $ uncurry (flip id)\n",
131
+
" \n",
132
+
" to :: Prop1 m -> Lem m\n",
133
+
" to (Prop1 i) = Lem $ fmap Left $ i (id, pure . fix)"
134
+
]
135
+
},
136
+
{
137
+
"cell_type": "code",
138
+
"execution_count": 5,
139
+
"metadata": {},
140
+
"outputs": [],
141
+
"source": [
142
+
"-- forall. P,Q. P -> - (- P /\\ B)\n",
143
+
"\n",
144
+
"newtype Prop2 m = \n",
145
+
" Prop2\n",
146
+
" (forall a b.\n",
147
+
" (a -> m (((a -> m Void), b) -> m Void)))\n",
148
+
" \n",
149
+
"-- proof, Prop2 <==> LEM\n",
150
+
"instance Monad m => Proof.Iso (Prop2 m) (Lem m) where\n",
151
+
" to :: Prop2 m -> Lem m\n",
152
+
" to (Prop2 p) = Lem $ pure $ Right proof where\n",
153
+
" proof :: a -> m Void\n",
154
+
" proof x = p x >>= ($ (proof, x))\n",
155
+
" \n",
156
+
" from :: Lem m -> Prop2 m\n",
157
+
" from (Lem l) = Prop2 $ flip fmap l . proof where\n",
158
+
" proof :: a -> Either a (a -> m Void) -> (((a -> m Void), b) -> m Void)\n",
159
+
" proof x = either (flip fst) (\\f _ -> f x)\n",
160
+
" "
161
+
]
162
+
},
163
+
{
164
+
"cell_type": "code",
165
+
"execution_count": 6,
166
+
"metadata": {},
167
+
"outputs": [],
168
+
"source": [
169
+
"-- forall. P,Q. - (P /\\ Q) -> (P -> - Q)\n",
170
+
"import Control.Applicative (liftA2)\n",
171
+
"\n",
172
+
"newtype Prop3 m = \n",
173
+
" Prop3\n",
174
+
" (forall a b.\n",
175
+
" ((a,b) -> m Void) -> m (a -> m (b -> m Void)))\n",
176
+
" \n",
177
+
"-- proof, Prop3 <==> LEM\n",
178
+
"instance Monad m => Proof.Iso (Prop3 m) (Lem m) where\n",
179
+
" to :: Prop3 m -> Lem m\n",
180
+
" to (Prop3 p) = Lem $ fmap Right $ proof >>= (\\f -> pure (liftA2 (>>=) f (flip id))) where\n",
181
+
" proof :: m (a -> m (a -> m Void))\n",
182
+
" proof = p (\\(x,y) -> proof >>= (($ y) =<<) . ($ x))\n",
183
+
" \n",
184
+
" from :: Lem m -> Prop3 m\n",
185
+
" from (Lem l) = Prop3 $ (\\f -> pure (\\a -> either (const . f . (a ,)) id <$> l))"
186
+
]
187
+
},
188
+
{
189
+
"cell_type": "code",
190
+
"execution_count": 7,
191
+
"metadata": {},
192
+
"outputs": [],
193
+
"source": [
194
+
"import Proof\n",
195
+
"-- forall. P,Q. -P /\\ -Q -> - (P \\/ Q)\n",
196
+
"\n",
197
+
"newtype Prop4 m = \n",
198
+
" Prop4\n",
199
+
" (forall a b.\n",
200
+
" ((a -> m Void , b -> m Void) -> m (Either a b -> m Void)))\n",
201
+
" \n",
202
+
"-- proof, Prop4 <==> LEM\n",
203
+
"instance Monad m => Proof.Iso (Prop4 m) (Lem m) where\n",
204
+
" to :: Prop4 m -> Lem m\n",
205
+
" to (Prop4 p) = Lem $ pure $ Right ((proof >>=) . flip id . Left) where\n",
206
+
" proof :: m (Either a a -> m Void)\n",
207
+
" proof = curry p ((proof >>=) . flip id . Left) ((proof >>=) . flip id . Right)\n",
208
+
" \n",
209
+
" from :: Lem m -> Prop4 m\n",
210
+
" from _ = Prop4 $ uncurry $ (pure .) . either"
211
+
]
212
+
},
213
+
{
214
+
"cell_type": "markdown",
215
+
"metadata": {},
216
+
"source": [
217
+
"---"
218
+
]
219
+
},
220
+
{
221
+
"cell_type": "markdown",
222
+
"metadata": {},
223
+
"source": [
224
+
"_This is an [IHaskell Notebook]() which is pretty cool for above kind of experiments. Much more feature rich than GHCi. I got the inspiration from [Vaibhav Sagar](https://twitter.com/vbhvsgr) who writes [all his posts](https://vaibhavsagar.com/) as IHaskell Notebooks._"
225
+
]
226
+
}
227
+
],
228
+
"metadata": {
229
+
"kernelspec": {
230
+
"display_name": "Haskell",
231
+
"language": "haskell",
232
+
"name": "haskell"
233
+
},
234
+
"language_info": {
235
+
"codemirror_mode": "ihaskell",
236
+
"file_extension": ".hs",
237
+
"name": "haskell",
238
+
"pygments_lexer": "Haskell",
239
+
"version": "8.4.4"
240
+
}
241
+
},
242
+
"nbformat": 4,
243
+
"nbformat_minor": 2
244
+
}
+23
updater
+23
updater
···
1
+
#! /usr/bin/env nix-shell
2
+
#! nix-shell -i bash
3
+
#! nix-shell -p curl jq nix
4
+
5
+
set -eufo pipefail
6
+
7
+
FILE=$1
8
+
PROJECT=$2
9
+
BRANCH=${3:-master}
10
+
11
+
OWNER=$(jq -r '.[$project].owner' --arg project "$PROJECT" < "$FILE")
12
+
REPO=$(jq -r '.[$project].repo' --arg project "$PROJECT" < "$FILE")
13
+
14
+
REV=$(curl "https://api.github.com/repos/$OWNER/$REPO/branches/$BRANCH" | jq -r '.commit.sha')
15
+
SHA256=$(nix-prefetch-url --unpack "https://github.com/$OWNER/$REPO/archive/$REV.tar.gz")
16
+
TJQ=$(jq '.[$project] = {owner: $owner, repo: $repo, rev: $rev, sha256: $sha256}' \
17
+
--arg project "$PROJECT" \
18
+
--arg owner "$OWNER" \
19
+
--arg repo "$REPO" \
20
+
--arg rev "$REV" \
21
+
--arg sha256 "$SHA256" \
22
+
< "$FILE")
23
+
[[ $? == 0 ]] && echo "${TJQ}" >| "$FILE"
+14
versions.json
+14
versions.json
···
1
+
{
2
+
"ihaskell": {
3
+
"owner": "gibiansky",
4
+
"repo": "IHaskell",
5
+
"rev": "376d108d1f034f4e9067f8d9e9ef7ddad2cce191",
6
+
"sha256": "0359rn46xaspzh96sspjwklazk4qljdw2xxchlw2jmfa173miq6a"
7
+
},
8
+
"nixpkgs": {
9
+
"owner": "NixOS",
10
+
"repo": "nixpkgs-channels",
11
+
"rev": "3a393eecafb3fcd9db5ff94783ddab0c55d15860",
12
+
"sha256": "1r7pycxxjcz3idyl35am4b4rdh4h5srd5r7w8msy2sc1sv830r30"
13
+
}
14
+
}