dubiouscript · April 15, 2019 11:17 · Dec 24, 2018 · Dec 21, 2018 · Dec 21, 2018 · Dec 21, 2018
diff --git a/category-theory-study-materials.org b/category-theory-study-materials.org
@@ -10,15 +10,6 @@
 - *PLT:* Programming Language Theory
 - *CS:* Computer Science
 
-** Bibliography
-
-- FPS: [[https://amzn.to/2R4RUJd][Functional Programming in Scala by Chiusano and Bjarnason]]
-- TDDI: [[https://amzn.to/2BzjfJH][Type Driven Development with Idris by Edwin Brady]]
-- TLT: [[https://amzn.to/2SgFqv5][The Little Typer by Friedman and Christiansen]]
-- CTC: [[https://amzn.to/2S9RNcA][Category Theory in Context (Aurora: Dover Modern Math Originals) by Emily Riehl]]
-- BCTCS: [[https://amzn.to/2QIT65j][Basic Category Theory for Computer Scientists (Foundations of Computing) by Benjamin Pierce]]
-- TAPL: [[https://amzn.to/2BB2fCV][Types and Programming Languages (The MIT Press) by Benjamin C. Pierce]]
-
 ** Background
 
 Here are my own experiences with study materials related to the field of Category Theory. Your mileage may vary (YMMV). Background: my bachelors degree was in mathematics so I was /once/ familiar with rigorous mathematics, especially proofs, etc but by the time I discovered the utility of Category Theory for my work as a software developer I had already been out of college for over a decade and my rigor level for mathematics had atrophied and needed practice to build up my reasoning muscles again. Practice really is the key to all of this, so it takes time but be patient.
@@ -30,7 +21,7 @@ My timeline for learning what I know now with the aim of internalizing understan
 - mid-2015-2016: I stupidly took a new job in yet another toxic software company yet I read TAPL (see below) - although not thoroughly - and FPS (see below) as well as experimenting with Idris via TDD book and dependent types which helped me flesh out my understanding on CT, how to use types more effectively, and desirable properties of type systems plus general FP techniques which are not entirely coupled yet have a large overlap of research and community.
 - since Q3 2016: delving into recursion schemes, reading more papers, attending graduate level courses (MGS), and attending ICFP sessions and workshops. Concepts from CT that I developed a deeper understanding of during this time were: limits, colimits, algebras, coalgebras, adjunctions, natural transformations. I still have a lot more to understand and cover but I do find myself identifying categorical patterns seen in the wild much more than I used to. A better understanding of lambda calculus allowed me to grok =Fix= and how that eliminates recursion on the data structure level by relating the same idea from the term-level in lambda calcululs (keywords: self-application, y-combinator, omega-combinator). A basic but more formal understanding of lambda calculus came from a course taken from Capretta at Midland Graduate School in April 2018.
 
-*** Learnings
+** Learnings
 
 Learning academic material in my 30s after a decade of professional experience - thinking that was all behind me - taught me a few things about how ineffective my learning attitudes and practices were as an adult. Below is a list of things I wish I knew when I started this journey in 2011:
 
@@ -44,33 +35,64 @@ Learning academic material in my 30s after a decade of professional experience -
 - Quiz yourself on the material you have recently encountered and revisit via self-testing until you don't even pause to answer. You can do this by writing questions for yourself the following day immediately after you have studied some material and/or immediately after listening, watching, or reading make notes in your own words (avoid highlighting as it gives you a false sense of understanding) and if possible convert to executable code or type definitions that type check that demonstrates your recent topic.
 - Come up with questions for further research. Add them as TODOs for a new day (some time in the next week) and schedule 15 minutes to find new material to answer your questions. Write notes and/or code to demonstrate the new learning from the research item.
 
-** For those with software development experience but not necessarily rigorous pure mathematics
+** Book Materials
+*** Bibliography
 
-*** [[https://amzn.to/2R4RUJd][Functional Programming in Scala by Chiusano and Bjarnason (aka FPS)]]
+- FPS: [[https://amzn.to/2R4RUJd][Functional Programming in Scala by Chiusano and Bjarnason]]
+- TDDI: [[https://amzn.to/2BzjfJH][Type Driven Development with Idris by Edwin Brady]]
+- TLT: [[https://amzn.to/2SgFqv5][The Little Typer by Friedman and Christiansen]]
+- CTC: [[https://amzn.to/2S9RNcA][Category Theory in Context (Aurora: Dover Modern Math Originals) by Emily Riehl]]
+- BCTCS: [[https://amzn.to/2QIT65j][Basic Category Theory for Computer Scientists (Foundations of Computing) by Benjamin Pierce]]
+- TAPL: [[https://amzn.to/2BB2fCV][Types and Programming Languages (The MIT Press) by Benjamin C. Pierce]]
+
+*** For those with software development experience but not necessarily rigorous pure mathematics
+
+**** [[https://amzn.to/2R4RUJd][Functional Programming in Scala by Chiusano and Bjarnason (aka FPS)]]
 
 A great FP text for the working Scala developer. Introducing a number of important fundamnetal ideas for FP. Some indirect references to CT. Do the exercises. Don't be passive consuming this material. You will get more out of the material if you do the exercises even the earlier chapters (even if you think you are "above" the earlier chapters; I suffered from this delusion until I reviewed the effectiveness of my learning strategies and rebooted).
 
-*** [[https://amzn.to/2BzjfJH][Type Driven Development with Idris by Edwin Brady]] (aka TDDI)
+**** [[https://amzn.to/2BzjfJH][Type Driven Development with Idris by Edwin Brady]] (aka TDDI)
 
 Learned a great deal about dependent types which I was a total n00b to at the time of first reading and also exercised my inductive definition muscles through the exercises. Again, work through the exercises, it will improve your understanding if dependent types and type directed programming is interesting to you. I always thought the phrase type-drive or type-directed over emphasized the type specification part while ignoring the huge benefit which is that you get program inference almost for free as long as you specify your program's type well enough. :)
 
-*** [[https://amzn.to/2SgFqv5][The Little Typer by Friedman and Christiansen]] (aka TLT)
+**** [[https://amzn.to/2SgFqv5][The Little Typer by Friedman and Christiansen]] (aka TLT)
 
 A fun exploration of dependently typed ideas and concepts through a scheme/Lisp-based language named Pie.
 
-** For those with some familiarity with Set theory and reading proofs
+*** For those with some familiarity with Set theory and reading proofs
 
-*** [[https://amzn.to/2S9RNcA][Category Theory in Context (Aurora: Dover Modern Math Originals) by Emily Riehl]] (aka CTC)
+**** [[https://amzn.to/2S9RNcA][Category Theory in Context (Aurora: Dover Modern Math Originals) by Emily Riehl]] (aka CTC)
 
 Lots of examples but many of the examples shown are from set/group theory or topological realms of mathematics. The many examples were very useful for me to help me see more deeply some patterns.
 
-*** [[https://amzn.to/2QIT65j][Basic Category Theory for Computer Scientists (Foundations of Computing) by Benjamin Pierce]] (aka BCTCS)
+**** [[https://amzn.to/2QIT65j][Basic Category Theory for Computer Scientists (Foundations of Computing) by Benjamin Pierce]] (aka BCTCS)
 
 Relatively approachable, good exercises, more directly applicable material for software developers than Riehl's book.
 
-** For those with a classical CS background (CS-oriented higher level mathematics)
+*** For those with a classical CS background (CS-oriented higher level mathematics)
 
-*** [[https://amzn.to/2BB2fCV][Types and Programming Languages (The MIT Press) by Benjamin C. Pierce]] (aka TAPL)
+**** [[https://amzn.to/2BB2fCV][Types and Programming Languages (The MIT Press) by Benjamin C. Pierce]] (aka TAPL)
 
 While not directly related to CT this book does relate to the programming language theory (PLT) which has a large overlap of research activities with applying CT to software development and CS generally.
 
+
+** Lecture Series
+
+*** Midland Graduate School (MGS) 2018
+
+- [[http://www.duplavis.com/venanzio/mgs_lambda/][Lambda Calculus by Capretta]]
+- [[http://www.cs.bham.ac.uk/~axj/pub/papers/Jung-2014-Teaching-denotational-semantics.pdf][Domain Theory and Denotational Semantics by Jung]]
+- [[http://www.cs.le.ac.uk/people/akurz/coalgebras-mgs2018.pdf][Coalgebra by Kurz]]
+- [[http://www.cs.le.ac.uk/people/rlc3/mgs/catTheoryLectures.xml][Category Theory by Crole]]
+- [[https://homotopytypetheory.org/book/][Univalent Foundations by Ahrens]]
+
+*** [[https://www.cs.uoregon.edu/research/summerschool/summer18/][Oregon Programming Languages Summer School (OPLSS) 2018]]
+
+TODO
+
+
+** Conference Talks/Slides (including videos)
+
+*** LambdaConf
+
+TODO
diff --git a/category-theory-study-materials.org b/category-theory-study-materials.org
@@ -25,7 +25,7 @@ Here are my own experiences with study materials related to the field of Categor
 
 My timeline for learning what I know now with the aim of internalizing understanding so I can more fluidly apply reasoning techniques was not efficient or particularly effective but I think it might benefit seeing where I went wrong:
 
-- 2011-2013: Started using Scalaz at work, learned the definition of a category and functor in a math sense and using concepts like =Functor=, =Applicative=, =ValidationNEL=, =Monoid=, =Semigroup=, etc and vaguely seeing how the software definitions mapped to mathemtical concepts but not deeply. Also developed intuitions for what the dreaded =Monad=. Through lots of pain and suffering from production bugs I learned deeply flawed most version of "Future" (and there were many at this time in the Scala ecosystem) were and how it was related to violating laws of common FP abstractions.
+- 2011-2013: Started using Scalaz at work, learned the definition of a category and functor in a math sense and using concepts like =Functor=, =Applicative=, =ValidationNEL=, =Monoid=, =Semigroup=, etc and vaguely seeing how the software definitions mapped to mathematical concepts but not deeply. I also developed intuitions for what the dreaded =Monad= was but got caught up in a lot of FP folklore (my advise is just focus on the fact that these are just abstractions with a precise mathematical definition that abide by certain mathematical laws). Through lots of pain and suffering from production bugs I learned deeply flawed most version of "Future" (and there were many at this time in the Scala ecosystem) were and how it was related to violating laws of common FP abstractions.
 - late 2013-2015: Bought Pierce's BCTCS (see below). Flicked through it and realized my mathematical reasoning skills had atrophied significantly. Demotivated by my lack of current rigor, I read only the first four chapters and then left it on the bookshelf for another year. Working as an SRE and then soon after that engineering manager at a toxic workplace that required I work very long hours: I read a couple of papers during this time related to CT, FP, type theory, and reasoning about programs but many were false starts at deeper understanding and I ended up revisiting a lot of this material after I switched jobs.
 - mid-2015-2016: I stupidly took a new job in yet another toxic software company yet I read TAPL (see below) - although not thoroughly - and FPS (see below) as well as experimenting with Idris via TDD book and dependent types which helped me flesh out my understanding on CT, how to use types more effectively, and desirable properties of type systems plus general FP techniques which are not entirely coupled yet have a large overlap of research and community.
 - since Q3 2016: delving into recursion schemes, reading more papers, attending graduate level courses (MGS), and attending ICFP sessions and workshops. Concepts from CT that I developed a deeper understanding of during this time were: limits, colimits, algebras, coalgebras, adjunctions, natural transformations. I still have a lot more to understand and cover but I do find myself identifying categorical patterns seen in the wild much more than I used to. A better understanding of lambda calculus allowed me to grok =Fix= and how that eliminates recursion on the data structure level by relating the same idea from the term-level in lambda calcululs (keywords: self-application, y-combinator, omega-combinator). A basic but more formal understanding of lambda calculus came from a course taken from Capretta at Midland Graduate School in April 2018.

diff --git a/category-theory-study-materials.org b/category-theory-study-materials.org
@@ -26,13 +26,13 @@ Here are my own experiences with study materials related to the field of Categor
 My timeline for learning what I know now with the aim of internalizing understanding so I can more fluidly apply reasoning techniques was not efficient or particularly effective but I think it might benefit seeing where I went wrong:
 
 - 2011-2013: Started using Scalaz at work, learned the definition of a category and functor in a math sense and using concepts like =Functor=, =Applicative=, =ValidationNEL=, =Monoid=, =Semigroup=, etc and vaguely seeing how the software definitions mapped to mathemtical concepts but not deeply. Also developed intuitions for what the dreaded =Monad=. Through lots of pain and suffering from production bugs I learned deeply flawed most version of "Future" (and there were many at this time in the Scala ecosystem) were and how it was related to violating laws of common FP abstractions.
-- late 2013-2015: Bought Pierce's BCTCS (see below). Flicked through it and realized my mathemtical reasoning skills had atrophied significantly. Demotivated by my lack of current rigor, I read only the first four chapters and then left it on the bookshelf for another year or so. Working as an SRE and then soon after that engineering manager at a toxic workplace that required I work very long hours, I read a couple of papers during this time related to CT, FP, type theory, and reasoning about programs but many were false starts at deeper understanding and I ended up revisiting a lot of this material after I switched jobs.
-- mid-2015-2016: I stupidly took a new job in yet another toxic software company yet I read TAPL (see below) - although not thoroughly - and FPS (see below) as well as experimenting with Idris via TDD book and dependent types which all helped me flesh out my understanding on CT, how to use types more effectively, and desirable properties of type systems plus general FP techniques which are not entirely coupled yet have a large overlap of research and community.
+- late 2013-2015: Bought Pierce's BCTCS (see below). Flicked through it and realized my mathematical reasoning skills had atrophied significantly. Demotivated by my lack of current rigor, I read only the first four chapters and then left it on the bookshelf for another year. Working as an SRE and then soon after that engineering manager at a toxic workplace that required I work very long hours: I read a couple of papers during this time related to CT, FP, type theory, and reasoning about programs but many were false starts at deeper understanding and I ended up revisiting a lot of this material after I switched jobs.
+- mid-2015-2016: I stupidly took a new job in yet another toxic software company yet I read TAPL (see below) - although not thoroughly - and FPS (see below) as well as experimenting with Idris via TDD book and dependent types which helped me flesh out my understanding on CT, how to use types more effectively, and desirable properties of type systems plus general FP techniques which are not entirely coupled yet have a large overlap of research and community.
 - since Q3 2016: delving into recursion schemes, reading more papers, attending graduate level courses (MGS), and attending ICFP sessions and workshops. Concepts from CT that I developed a deeper understanding of during this time were: limits, colimits, algebras, coalgebras, adjunctions, natural transformations. I still have a lot more to understand and cover but I do find myself identifying categorical patterns seen in the wild much more than I used to. A better understanding of lambda calculus allowed me to grok =Fix= and how that eliminates recursion on the data structure level by relating the same idea from the term-level in lambda calcululs (keywords: self-application, y-combinator, omega-combinator). A basic but more formal understanding of lambda calculus came from a course taken from Capretta at Midland Graduate School in April 2018.
 
 *** Learnings
 
-Learning academic material in my 30s after a decade of professional experience - thinking that was all behind me - taught me a few things about how ineffective my learning attitudes and practices were as an adult. Below is a list of things I wish I practiced when I started this journey in 2011:
+Learning academic material in my 30s after a decade of professional experience - thinking that was all behind me - taught me a few things about how ineffective my learning attitudes and practices were as an adult. Below is a list of things I wish I knew when I started this journey in 2011:
 
 - Do more practice of the material under study. This includes doing exercises from the books, especially in code if possible.
 - Take breaks and chunk the study material.

diff --git a/category-theory-study-materials.org b/category-theory-study-materials.org
@@ -25,7 +25,7 @@ Here are my own experiences with study materials related to the field of Categor
 
 My timeline for learning what I know now with the aim of internalizing understanding so I can more fluidly apply reasoning techniques was not efficient or particularly effective but I think it might benefit seeing where I went wrong:
 
-- 2011-2013: Started using Scalaz at work, learned the definition of a category and functor in a math sense and using concepts like =Functor=, =Applicative=, =ValidationNEL=, =Monoid=, =Semigroup=, etc and vaguely seeing how the software definitions mapped to mathemtical concepts but not deeply. Also developed intuitions for what the dreaded =Monad=. Through lots of pain and suffering from production bugs I learned deeply flawed most version of "Future" (and there were many at this time in the Scala ecosystem) were.
+- 2011-2013: Started using Scalaz at work, learned the definition of a category and functor in a math sense and using concepts like =Functor=, =Applicative=, =ValidationNEL=, =Monoid=, =Semigroup=, etc and vaguely seeing how the software definitions mapped to mathemtical concepts but not deeply. Also developed intuitions for what the dreaded =Monad=. Through lots of pain and suffering from production bugs I learned deeply flawed most version of "Future" (and there were many at this time in the Scala ecosystem) were and how it was related to violating laws of common FP abstractions.
 - late 2013-2015: Bought Pierce's BCTCS (see below). Flicked through it and realized my mathemtical reasoning skills had atrophied significantly. Demotivated by my lack of current rigor, I read only the first four chapters and then left it on the bookshelf for another year or so. Working as an SRE and then soon after that engineering manager at a toxic workplace that required I work very long hours, I read a couple of papers during this time related to CT, FP, type theory, and reasoning about programs but many were false starts at deeper understanding and I ended up revisiting a lot of this material after I switched jobs.
 - mid-2015-2016: I stupidly took a new job in yet another toxic software company yet I read TAPL (see below) - although not thoroughly - and FPS (see below) as well as experimenting with Idris via TDD book and dependent types which all helped me flesh out my understanding on CT, how to use types more effectively, and desirable properties of type systems plus general FP techniques which are not entirely coupled yet have a large overlap of research and community.
 - since Q3 2016: delving into recursion schemes, reading more papers, attending graduate level courses (MGS), and attending ICFP sessions and workshops. Concepts from CT that I developed a deeper understanding of during this time were: limits, colimits, algebras, coalgebras, adjunctions, natural transformations. I still have a lot more to understand and cover but I do find myself identifying categorical patterns seen in the wild much more than I used to. A better understanding of lambda calculus allowed me to grok =Fix= and how that eliminates recursion on the data structure level by relating the same idea from the term-level in lambda calcululs (keywords: self-application, y-combinator, omega-combinator). A basic but more formal understanding of lambda calculus came from a course taken from Capretta at Midland Graduate School in April 2018.

diff --git a/category-theory-study-materials.org b/category-theory-study-materials.org
@@ -12,12 +12,12 @@
 
 ** Bibliography
 
-*** FPS: [[https://amzn.to/2R4RUJd][Functional Programming in Scala by Chiusano and Bjarnason]]
-*** TDDI: [[https://amzn.to/2BzjfJH][Type Driven Development with Idris by Edwin Brady]]
-*** TLT: [[https://amzn.to/2SgFqv5][The Little Typer by Friedman and Christiansen]]
-*** CTC: [[https://amzn.to/2S9RNcA][Category Theory in Context (Aurora: Dover Modern Math Originals) by Emily Riehl]]
-*** BCTCS: [[https://amzn.to/2QIT65j][Basic Category Theory for Computer Scientists (Foundations of Computing) by Benjamin Pierce]]
-*** TAPL: [[https://amzn.to/2BB2fCV][Types and Programming Languages (The MIT Press) by Benjamin C. Pierce]]
+- FPS: [[https://amzn.to/2R4RUJd][Functional Programming in Scala by Chiusano and Bjarnason]]
+- TDDI: [[https://amzn.to/2BzjfJH][Type Driven Development with Idris by Edwin Brady]]
+- TLT: [[https://amzn.to/2SgFqv5][The Little Typer by Friedman and Christiansen]]
+- CTC: [[https://amzn.to/2S9RNcA][Category Theory in Context (Aurora: Dover Modern Math Originals) by Emily Riehl]]
+- BCTCS: [[https://amzn.to/2QIT65j][Basic Category Theory for Computer Scientists (Foundations of Computing) by Benjamin Pierce]]
+- TAPL: [[https://amzn.to/2BB2fCV][Types and Programming Languages (The MIT Press) by Benjamin C. Pierce]]
 
 ** Background
 

diff --git a/category-theory-study-materials.org b/category-theory-study-materials.org
@@ -0,0 +1,76 @@
+* Category Theory and Functional Programming Study Materials
+
+** Acronyms/Terms
+
+- *CT:* Category Theory
+- *FP:* Functional Programming (typically meaning more pure functional programming)
+- *TFP:* Total Functional Programming
+- *TDD:* Type Driven Development (e.g. via Idris or Agda)
+- *TT:* Type Theory
+- *PLT:* Programming Language Theory
+- *CS:* Computer Science
+
+** Bibliography
+
+*** FPS: [[https://amzn.to/2R4RUJd][Functional Programming in Scala by Chiusano and Bjarnason]]
+*** TDDI: [[https://amzn.to/2BzjfJH][Type Driven Development with Idris by Edwin Brady]]
+*** TLT: [[https://amzn.to/2SgFqv5][The Little Typer by Friedman and Christiansen]]
+*** CTC: [[https://amzn.to/2S9RNcA][Category Theory in Context (Aurora: Dover Modern Math Originals) by Emily Riehl]]
+*** BCTCS: [[https://amzn.to/2QIT65j][Basic Category Theory for Computer Scientists (Foundations of Computing) by Benjamin Pierce]]
+*** TAPL: [[https://amzn.to/2BB2fCV][Types and Programming Languages (The MIT Press) by Benjamin C. Pierce]]
+
+** Background
+
+Here are my own experiences with study materials related to the field of Category Theory. Your mileage may vary (YMMV). Background: my bachelors degree was in mathematics so I was /once/ familiar with rigorous mathematics, especially proofs, etc but by the time I discovered the utility of Category Theory for my work as a software developer I had already been out of college for over a decade and my rigor level for mathematics had atrophied and needed practice to build up my reasoning muscles again. Practice really is the key to all of this, so it takes time but be patient.
+
+My timeline for learning what I know now with the aim of internalizing understanding so I can more fluidly apply reasoning techniques was not efficient or particularly effective but I think it might benefit seeing where I went wrong:
+
+- 2011-2013: Started using Scalaz at work, learned the definition of a category and functor in a math sense and using concepts like =Functor=, =Applicative=, =ValidationNEL=, =Monoid=, =Semigroup=, etc and vaguely seeing how the software definitions mapped to mathemtical concepts but not deeply. Also developed intuitions for what the dreaded =Monad=. Through lots of pain and suffering from production bugs I learned deeply flawed most version of "Future" (and there were many at this time in the Scala ecosystem) were.
+- late 2013-2015: Bought Pierce's BCTCS (see below). Flicked through it and realized my mathemtical reasoning skills had atrophied significantly. Demotivated by my lack of current rigor, I read only the first four chapters and then left it on the bookshelf for another year or so. Working as an SRE and then soon after that engineering manager at a toxic workplace that required I work very long hours, I read a couple of papers during this time related to CT, FP, type theory, and reasoning about programs but many were false starts at deeper understanding and I ended up revisiting a lot of this material after I switched jobs.
+- mid-2015-2016: I stupidly took a new job in yet another toxic software company yet I read TAPL (see below) - although not thoroughly - and FPS (see below) as well as experimenting with Idris via TDD book and dependent types which all helped me flesh out my understanding on CT, how to use types more effectively, and desirable properties of type systems plus general FP techniques which are not entirely coupled yet have a large overlap of research and community.
+- since Q3 2016: delving into recursion schemes, reading more papers, attending graduate level courses (MGS), and attending ICFP sessions and workshops. Concepts from CT that I developed a deeper understanding of during this time were: limits, colimits, algebras, coalgebras, adjunctions, natural transformations. I still have a lot more to understand and cover but I do find myself identifying categorical patterns seen in the wild much more than I used to. A better understanding of lambda calculus allowed me to grok =Fix= and how that eliminates recursion on the data structure level by relating the same idea from the term-level in lambda calcululs (keywords: self-application, y-combinator, omega-combinator). A basic but more formal understanding of lambda calculus came from a course taken from Capretta at Midland Graduate School in April 2018.
+
+*** Learnings
+
+Learning academic material in my 30s after a decade of professional experience - thinking that was all behind me - taught me a few things about how ineffective my learning attitudes and practices were as an adult. Below is a list of things I wish I practiced when I started this journey in 2011:
+
+- Do more practice of the material under study. This includes doing exercises from the books, especially in code if possible.
+- Take breaks and chunk the study material.
+- Read around the topic under study actively seeking out differing perspectives (e.g. a mathematical perspective vs a CS perspective vs a software development perspective).
+- Practice, practice, practice!
+- Carve out small periods of time each or every other day to study material and revisit the material to make sure you retain it for longer.
+- Identify what other topics are related to the current study topic and understand how they are related.
+- Sleep between your study sessions on a topic.
+- Quiz yourself on the material you have recently encountered and revisit via self-testing until you don't even pause to answer. You can do this by writing questions for yourself the following day immediately after you have studied some material and/or immediately after listening, watching, or reading make notes in your own words (avoid highlighting as it gives you a false sense of understanding) and if possible convert to executable code or type definitions that type check that demonstrates your recent topic.
+- Come up with questions for further research. Add them as TODOs for a new day (some time in the next week) and schedule 15 minutes to find new material to answer your questions. Write notes and/or code to demonstrate the new learning from the research item.
+
+** For those with software development experience but not necessarily rigorous pure mathematics
+
+*** [[https://amzn.to/2R4RUJd][Functional Programming in Scala by Chiusano and Bjarnason (aka FPS)]]
+
+A great FP text for the working Scala developer. Introducing a number of important fundamnetal ideas for FP. Some indirect references to CT. Do the exercises. Don't be passive consuming this material. You will get more out of the material if you do the exercises even the earlier chapters (even if you think you are "above" the earlier chapters; I suffered from this delusion until I reviewed the effectiveness of my learning strategies and rebooted).
+
+*** [[https://amzn.to/2BzjfJH][Type Driven Development with Idris by Edwin Brady]] (aka TDDI)
+
+Learned a great deal about dependent types which I was a total n00b to at the time of first reading and also exercised my inductive definition muscles through the exercises. Again, work through the exercises, it will improve your understanding if dependent types and type directed programming is interesting to you. I always thought the phrase type-drive or type-directed over emphasized the type specification part while ignoring the huge benefit which is that you get program inference almost for free as long as you specify your program's type well enough. :)
+
+*** [[https://amzn.to/2SgFqv5][The Little Typer by Friedman and Christiansen]] (aka TLT)
+
+A fun exploration of dependently typed ideas and concepts through a scheme/Lisp-based language named Pie.
+
+** For those with some familiarity with Set theory and reading proofs
+
+*** [[https://amzn.to/2S9RNcA][Category Theory in Context (Aurora: Dover Modern Math Originals) by Emily Riehl]] (aka CTC)
+
+Lots of examples but many of the examples shown are from set/group theory or topological realms of mathematics. The many examples were very useful for me to help me see more deeply some patterns.
+
+*** [[https://amzn.to/2QIT65j][Basic Category Theory for Computer Scientists (Foundations of Computing) by Benjamin Pierce]] (aka BCTCS)
+
+Relatively approachable, good exercises, more directly applicable material for software developers than Riehl's book.
+
+** For those with a classical CS background (CS-oriented higher level mathematics)
+
+*** [[https://amzn.to/2BB2fCV][Types and Programming Languages (The MIT Press) by Benjamin C. Pierce]] (aka TAPL)
+
+While not directly related to CT this book does relate to the programming language theory (PLT) which has a large overlap of research activities with applying CT to software development and CS generally.
+