mharris717/messages.md

## messages.md

      
    Raw
  

              messages.md
            
          
    Just tried to put this in a more readable format: https://github.com/svanderbleek/haskellandchill.com/blob/master/a-conversation-about-oop-vs-fp-turns-constructive.md


Person
Time
Message


sagar
10:47
why is that, why is OOP trash


katychuang
10:48
excellent question


katychuang
10:49
I've been told FP and OOP are different paradigms


katychuang
10:52
I'm going to butcher a quote from a talk by Evie so I'm going to paraphrase… She said something like when you work with OOP you create lots of objects and rules on how they should interact and yet somehow end up having to touch each other a lot and inappropriately


katychuang
10:53
On the other hand FP (especially Haskell) is like working with shapes, like that baby shape fitting toy where you focus more on fitting the type parameters correctly


katychuang
10:56
I think of programming as building a piping system. FP (especially strongly typed FP) makes it more idiot proof because the connectors are more obvious. But I don't know if my mental model fits for the breakdown of OOP to FP… Clojure is a dynamically typed FP language for example


sagar
10:57
interesting


pedrofurla
10:58
katychuang where that paraphrasing from?


katychuang
10:58
from Evie, she gave a lightning talk months ago


sagar
10:58
because I want to start coding professionally,and I'm working for a company and they're happy to let me do intern stuff for their JS & Python so I was reading those but it was like >_>


sagar
10:58
Haskell I find much more appealing I don't know why


sagar
10:59
They have scala here too which seems like a reasonable middle ground but all the scala programmers here are ex java and keep giving me java examples or talking about the jvm


m
10:59
i've done production level java


m
10:59
and it's a goddamn jungle


pedrofurla
10:59
I good way to see what I think you are trying to say is by writing an interpreter in OO vs FP


katychuang
10:59
nod I personally wouldn't call OOP trash, a lot of companies use OOP and they make lots of money… and also have huge teams and a lot of documentation. It's just gooey-er to work with


pedrofurla
11:00
m: it's a jungle out there


katychuang
11:00
haha


m
11:00
The problem is once the Java structure gets bloated with enough objects and inheritance rules


sagar
11:00
java is just absurd. right from syntax and the whole class system. seems like a roundabout way of doing things.


m
11:00
it becomes hard to really build on


katychuang
11:00
jenga


sagar
11:00
that's actually one of the key projects this quarter lol


m
11:00
^^^


m
11:00
Jenga is the nail on the head


pedrofurla
11:01
more like the Cthulhu lair


katychuang
11:01
it's nice to work with the reliability haskell provides. cabal on the other hand is not so reliable 🙂


m
11:02
The appeal to me was watching the fluidity of someone programming in Haskell


m
11:02
it had an elegance to it


katychuang
11:03
oh yes. i was sold on the Maybe type


m
11:03
i was sold on not making folders of class files


katychuang
11:03
haha that's a good one also


katychuang
11:04
the brevity was a breath of fresh air


horrorcheck
11:04
I really like OOP…. I just like FP too


katychuang
11:06
😃


horrorcheck
11:06
(that doesn't mean I'm going to use Scala — I like hotdogs and ice cream but I'm not eating hot dog-flavored ice cream)


katychuang
11:06
haha good analogy


haskellandchill
11:09
OOP has cool stories, FP has math


haskellandchill
11:09
also you can provide a reasonable formal semantics for OOP in FP


katychuang
11:10
@sagar sometimes people are biased. obviously we all love haskell in here lol (edited)


sagar
11:10
lol


haskellandchill
11:10
I did OOP for 6 years, that's my bias


katychuang
11:10
@haskellandchill in one language or multiple OOP languages? (edited)


sagar
11:11
Scala isYUGE though omg


sagar
11:11
for monies


haskellandchill
11:11
Ruby, with a heavy Smalltalk influence


sagar
11:11
and career etc


haskellandchill
11:11
Scala is a good career choice 👍


m
11:11
thank Java for that @sagar lol


haskellandchill
11:12
I personally can't stand Scala, but lots of good books written for it


m
11:12
it's taaaaainted


haskellandchill
11:12
incidental complexity, subtyping (ew)


haskellandchill
11:13
subtyping with contravariance 💥


pedrofurla
11:13
we do Scala where i work, and I assure you we only have hotdogs


katychuang
11:13
haha


katychuang
11:14
@haskellandchill those words.. :whoosh:


pedrofurla
11:14
@haskellandchill yep, that's why we stick only with the hotdogs


haskellandchill
11:14
Haskell is far behind Scala in libraries, that's very true


pedrofurla
11:14
yah, but most scala libraries aren't great or are just plain bad java libraries


haskellandchill
11:15
¯_(ツ)_/¯


haskellandchill
11:15
I'm trying to be nice


m
11:15
being nice is overrated


m
11:15
i think scala has a horrendous type system


m
11:16
now i'll be nice


haskellandchill
11:16
well… it's important, these are peoples livelihoods, it can get emotional


haskellandchill
11:16
I almost got kicked out of a conference so I'm adjusting my approach


pedrofurla
11:16
subtyping and parametricity has a lot of potential for really big mess


m
11:16
goes back to what @haskellandchill said about incidental complexity


pedrofurla
11:16
@haskellandchill by saying scala sucks?


haskellandchill
11:16
also I'm not as funny as I think I am and it's the internet


pedrofurla
11:17
well Scala sucks


haskellandchill
11:17
just talking about programming languages 😇


katychuang
11:17
hmm… would it be better to try to keep conversation in here fairly conducive to learning haskell rather than flaming other languages?


m
11:17
yes


haskellandchill
11:17
definitely 👍 (edited)


katychuang
11:18
so what are these big words that were dropped in here


sagar
11:18
🔥 🚒


haskellandchill
11:18
if you're learning Haskell you don't need to know about subtyping


sagar
11:18
CONTRAVARIANCE good god.


katychuang
11:18
contravariance? i've never heard of that


haskellandchill
11:18
contravariance is important


haskellandchill
11:18
if you know Functor you can discuss (edited)


pedrofurla
11:18
-variance


m
11:19
parametricity is a good one


haskellandchill
11:19
```


pedrofurla
11:19
covariance is the first


haskellandchill
11:19
first is covariant, second is contravariant


pedrofurla
11:19
contra- is the se...


haskellandchill
11:20
yup, usually you don't say covariant, just normal functor


pedrofurla
11:20
but the variance thing in Scala is relating to subtyping and type parameters


haskellandchill
11:20
yeah but as we are Haskell focused, we can just ignore all that 😄


haskellandchill
11:20
which is awesome less stuff to learn


pedrofurla
11:21
A <: B, F[A] <: F[B]


haskellandchill
11:21
god no please no


pedrofurla
11:21
A <: B, F[B] <: F[A]


pedrofurla
11:21
heheh


haskellandchill
11:21
any way if anyone isn't solid on reading haskell type signatures


haskellandchill
11:22
you have an a, a b, and a f a


haskellandchill
11:22
you get an f b


katychuang
11:22
i remember it taking a while to learn how to read haskell type signatures 😃


haskellandchill
11:22
thats normal functor


haskellandchill
11:22
you have an a, a b, and a f b


katychuang
11:22
f a and f b are functions btw


haskellandchill
11:22
you get a f a, that's contra


haskellandchill
11:22
f is a type level function and a is a type


katychuang
11:23
oh right that confused me


pedrofurla
11:23
type constructor, please


m
11:23
:whoosh:


haskellandchill
11:23
f a is f applied to a


haskellandchill
11:23
I prefer the perspective of type level functions


pedrofurla
11:23
a applied to f


pedrofurla
11:23
the arguments are what are applied


haskellandchill
11:23
huh?


pedrofurla
11:24
f a, a applied to f


haskellandchill
11:24
we usually say a function is applied to its arguments


haskellandchill
11:24
but either way


pedrofurla
11:24
nopes


haskellandchill
11:24
no problem boss 😉


katychuang
11:25
type constructor = type level functions? is that the conclusion


pedrofurla
11:25
omg, you are right, @haskellandchill https://en.wikipedia.org/wiki/Function_application


haskellandchill
11:25
I know I'm right


haskellandchill
11:25
thanks 🙂


haskellandchill
11:25
a type constructor is a kind of type level function


haskellandchill
11:25
there are others


haskellandchill
11:26
don't need to go into all the type level stuff, it can get complex quick and haskell isn't the best language to express things there


haskellandchill
11:26
key takeaway is you have functions from values to values


haskellandchill
11:27
and also functions from types to types


haskellandchill
11:27
Haskell gives you a very nice lambda calculus for both


haskellandchill
11:28
it's hard for beginners to see where you are working with values, and where you are working with types, but it is crucial to learn the distinction


haskellandchill
11:28
lots of Haskell examples use the same letter for the type and value so it's easy to get confused


haskellandchill
11:29
```


katychuang
11:32
i'm confused again


m
11:32
:whoosh:


haskellandchill
11:43
that just means I failed 😞 best done with a whiteboard


haskellandchill
11:44
I


haskellandchill
11:44
those a's mean different things


haskellandchill
11:44
II


haskellandchill
11:44
those f's mean different things


haskellandchill
11:45
it is confusing


haskellandchill
11:45
but it is also elegant


haskellandchill
11:45
you need to have the concept of a type judgement


haskellandchill
11:47
in I we have judgment a:a


haskellandchill
11:47
in II we have judgement a:f a


haskellandchill
11:47
the a before : is a value


haskellandchill
11:48
after : the a is a type


haskellandchill
11:48
value:type is a type judgement


m
11:48
i think that makes more sense


sagar
11:50
what are we judging


katychuang
11:50
i don't understand the part where you said “type judgement” - is the compiler making judgements?


sagar
11:51
this is very useful


haskellandchill
11:51
anyone can make a judgement


haskellandchill
11:51
you can do haskell by hand


haskellandchill
11:51
the compiler checks our judgements


haskellandchill
11:51
and infers judgements when we are not explicit


sagar
11:51
oh


haskellandchill
11:51
this is called type checking and type inference, respectively


sagar
11:51
is that like type casting


haskellandchill
11:51
no


sagar
11:51
like implicitly it assumes a type


haskellandchill
11:52
type casting does not exist in Haskell


sagar
11:52
if a type isn't specified (edited)


haskellandchill
11:52
it is unsafe


haskellandchill
11:52
it's inference, not casting


haskellandchill
11:52
you infer a type, then check your inference


haskellandchill
11:52
with casting you force a type from another type


sagar
11:52
ok interesting


sagar
11:52
what's a good 101 on this inference stuff


haskellandchill
11:52
doesn't exist


sagar
11:53
LOL


sagar
11:53
but interesting distinction


haskellandchill
11:53
Proofs and Types


haskellandchill
11:53
but it's more advanced


haskellandchill
11:53
by Jean-Yves Girard, not beginner friendly


sagar
11:53
so - just for mental models sake - inference is like casting except nothing is cast, it is infered and cheked and if the check fails then no compile


haskellandchill
11:53
inference is not like casting


sagar
11:53
where "inference" is the compiler going "oh this variable might be of x type" ?


haskellandchill
11:54
not really


sagar
11:54
hmm ok erases mental blackboard


haskellandchill
11:54
first you say ok it is of type x


haskellandchill
11:54
where x is a type variable


sagar
11:54
so int x


haskellandchill
11:54
then you use unification to constrain the concrete type of type variable x


haskellandchill
11:55
unification is a tool from logic


haskellandchill
11:55
you get two sides of an equation


haskellandchill
11:55
for example


haskellandchill
11:55
Int = x


haskellandchill
11:55
then you can infer type variable x is concrete type Int


katychuang
11:56
-- this is how I read it


haskellandchill
11:56
ok thanks @katychuang let me clarify


haskellandchill
11:56
```


katychuang
11:56
aha!


katychuang
11:57
so not exactly haskell syntax just yet


haskellandchill
11:57
I'm talking at a meta level


haskellandchill
11:57
very informally


katychuang
11:57
ahh got it


haskellandchill
11:58
@sager if you want to know more and are comfortable with Haskell syntax I can point you to some examples


haskellandchill
11:58
er @sagar


sagar
11:58
this is great


haskellandchill
11:58
it's fun to work through type constraint unification


haskellandchill
11:58
a few Haskell books have chapters on it that are very instructive


sagar
11:59
i don't think i'm that comfortable yet, i just finished the lambda calculus stuff. I have an undergrad in electronics engineering from over 10 years ago so i'm pretty happy in mathland, programming land not so much unless we're working with PLC's


haskellandchill
11:59
ok, yes learning to hold off on advanced things is key


haskellandchill
11:59
you can't just try and learn everything, it's overwhelming


katychuang
11:59
I feel like I need a brief refresher on unification - where is it from, do mathematicians use it?


haskellandchill
11:59
unification comes from logic, it is the basis of something like Prolog


sagar
12:00
the first chapter of the book took me back to like 11th grade heh functions, domains etc


haskellandchill
12:00
https://en.wikipedia.org/wiki/Unification_(computer_science)


haskellandchill
12:00
wikipedia page is very good


sagar
12:00
when i am better at it - @haskellandchill would you like to collaborate on a 101 medium blog post


haskellandchill
12:00
certainly


sagar
12:00
awesome


haskellandchill
12:01
I was going to edit some of this into “A Conversation About …” something ha


katychuang
12:01
👍 👍


katychuang
12:01
i see a bunch of greek letters on that wikipedia page


haskellandchill
12:01
yup


haskellandchill
12:02
> For example, using x,y,z as variables, the singleton equation set { cons(x,cons(x,nil)) = cons(2,y) } is a syntactic first-order unification problem that has the substitution { x ↦ 2, y ↦ cons(2,nil) } as its only solution. The syntactic first-order unification problem { y = cons(2,y) } has no solution over the set of finite terms; however, it has the single solution { y ↦ cons(2,cons(2,cons(2,...))) } over the set of infinite trees. The semantic first-order unification problem { a⋅x = x⋅a } has each substitution of the form { x ↦ a⋅...⋅a } as a solution in a semigroup, i.e. if (⋅) is considered associative; the same problem, viewed in an abelian group, where (⋅) is considered also commutative, has any substitution at all as a solution. The singleton set { a = y(x) } is a syntactic second-order unification problem, since y is a function variable. One solution is { x ↦ a, y ↦ (identity function) }; another one is { y ↦ (constant function mapping each value to a), x ↦ (any value) }.


sagar
12:02
i didn't know the word ofr it was unification  i always called it resolving an expression


sagar
12:02
from high school stuff


haskellandchill
12:02
that's a good section to try and understand, let me know if you have questions


katychuang
12:04
it's a challenge to read. i think in pictures and this is all text


haskellandchill
12:04
yea I want to do visualizations


haskellandchill
12:05
it's ok to accept you can't aren't prepared for the formalism and move on


haskellandchill
12:05
that wikipedia page isn't going anywhere 😄


katychuang
12:05
It's cool that John Alan Robinson came up with the unification algorithm, contributing to foundations of automated theorem proving. That gives some context


katychuang
12:06
Now I see unification is important as far as having a premise that the machine can compute the logic (I assumed it was a given that computers can compute as a millennial)


katychuang
12:06
So yes, moving on 🙂


pedrofurla
12:10
wow, the conversation changed drastically
Person	Time	Message
sagar	10:47	why is that, why is OOP trash
katychuang	10:48	excellent question
katychuang	10:49	I've been told FP and OOP are different paradigms
katychuang	10:52	I'm going to butcher a quote from a talk by Evie so I'm going to paraphrase… She said something like when you work with OOP you create lots of objects and rules on how they should interact and yet somehow end up having to touch each other a lot and inappropriately
katychuang	10:53	On the other hand FP (especially Haskell) is like working with shapes, like that baby shape fitting toy where you focus more on fitting the type parameters correctly
katychuang	10:56	I think of programming as building a piping system. FP (especially strongly typed FP) makes it more idiot proof because the connectors are more obvious. But I don't know if my mental model fits for the breakdown of OOP to FP… Clojure is a dynamically typed FP language for example
sagar	10:57	interesting
pedrofurla	10:58	katychuang where that paraphrasing from?
katychuang	10:58	from Evie, she gave a lightning talk months ago
sagar	10:58	because I want to start coding professionally,and I'm working for a company and they're happy to let me do intern stuff for their JS & Python so I was reading those but it was like >_>
sagar	10:58	Haskell I find much more appealing I don't know why
sagar	10:59	They have scala here too which seems like a reasonable middle ground but all the scala programmers here are ex java and keep giving me java examples or talking about the jvm
m	10:59	i've done production level java
m	10:59	and it's a goddamn jungle
pedrofurla	10:59	I good way to see what I think you are trying to say is by writing an interpreter in OO vs FP
katychuang	10:59	nod I personally wouldn't call OOP trash, a lot of companies use OOP and they make lots of money… and also have huge teams and a lot of documentation. It's just gooey-er to work with
pedrofurla	11:00	m: it's a jungle out there
katychuang	11:00	haha
m	11:00	The problem is once the Java structure gets bloated with enough objects and inheritance rules
sagar	11:00	java is just absurd. right from syntax and the whole class system. seems like a roundabout way of doing things.
m	11:00	it becomes hard to really build on
katychuang	11:00	jenga
sagar	11:00	that's actually one of the key projects this quarter lol
m	11:00	^^^
m	11:00	Jenga is the nail on the head
pedrofurla	11:01	more like the Cthulhu lair
katychuang	11:01	it's nice to work with the reliability haskell provides. cabal on the other hand is not so reliable 🙂
m	11:02	The appeal to me was watching the fluidity of someone programming in Haskell
m	11:02	it had an elegance to it
katychuang	11:03	oh yes. i was sold on the Maybe type
m	11:03	i was sold on not making folders of class files
katychuang	11:03	haha that's a good one also
katychuang	11:04	the brevity was a breath of fresh air
horrorcheck	11:04	I really like OOP…. I just like FP too
katychuang	11:06	😃
horrorcheck	11:06	(that doesn't mean I'm going to use Scala — I like hotdogs and ice cream but I'm not eating hot dog-flavored ice cream)
katychuang	11:06	haha good analogy
haskellandchill	11:09	OOP has cool stories, FP has math
haskellandchill	11:09	also you can provide a reasonable formal semantics for OOP in FP
katychuang	11:10	@sagar sometimes people are biased. obviously we all love haskell in here lol (edited)
sagar	11:10	lol
haskellandchill	11:10	I did OOP for 6 years, that's my bias
katychuang	11:10	@haskellandchill in one language or multiple OOP languages? (edited)
sagar	11:11	Scala isYUGE though omg
sagar	11:11	for monies
haskellandchill	11:11	Ruby, with a heavy Smalltalk influence
sagar	11:11	and career etc
haskellandchill	11:11	Scala is a good career choice 👍
m	11:11	thank Java for that @sagar lol
haskellandchill	11:12	I personally can't stand Scala, but lots of good books written for it
m	11:12	it's taaaaainted
haskellandchill	11:12	incidental complexity, subtyping (ew)
haskellandchill	11:13	subtyping with contravariance 💥
pedrofurla	11:13	we do Scala where i work, and I assure you we only have hotdogs
katychuang	11:13	haha
katychuang	11:14	@haskellandchill those words.. :whoosh:
pedrofurla	11:14	@haskellandchill yep, that's why we stick only with the hotdogs
haskellandchill	11:14	Haskell is far behind Scala in libraries, that's very true
pedrofurla	11:14	yah, but most scala libraries aren't great or are just plain bad java libraries
haskellandchill	11:15	¯_(ツ)_/¯
haskellandchill	11:15	I'm trying to be nice
m	11:15	being nice is overrated
m	11:15	i think scala has a horrendous type system
m	11:16	now i'll be nice
haskellandchill	11:16	well… it's important, these are peoples livelihoods, it can get emotional
haskellandchill	11:16	I almost got kicked out of a conference so I'm adjusting my approach
pedrofurla	11:16	subtyping and parametricity has a lot of potential for really big mess
m	11:16	goes back to what @haskellandchill said about incidental complexity
pedrofurla	11:16	@haskellandchill by saying scala sucks?
haskellandchill	11:16	also I'm not as funny as I think I am and it's the internet
pedrofurla	11:17	well Scala sucks
haskellandchill	11:17	just talking about programming languages 😇
katychuang	11:17	hmm… would it be better to try to keep conversation in here fairly conducive to learning haskell rather than flaming other languages?
m	11:17	yes
haskellandchill	11:17	definitely 👍 (edited)
katychuang	11:18	so what are these big words that were dropped in here
sagar	11:18	🔥 🚒
haskellandchill	11:18	if you're learning Haskell you don't need to know about subtyping
sagar	11:18	CONTRAVARIANCE good god.
katychuang	11:18	contravariance? i've never heard of that
haskellandchill	11:18	contravariance is important
haskellandchill	11:18	if you know Functor you can discuss (edited)
pedrofurla	11:18	-variance
m	11:19	parametricity is a good one
haskellandchill	11:19	```
pedrofurla	11:19	covariance is the first
haskellandchill	11:19	first is covariant, second is contravariant
pedrofurla	11:19	contra- is the se...
haskellandchill	11:20	yup, usually you don't say covariant, just normal functor
pedrofurla	11:20	but the variance thing in Scala is relating to subtyping and type parameters
haskellandchill	11:20	yeah but as we are Haskell focused, we can just ignore all that 😄
haskellandchill	11:20	which is awesome less stuff to learn
pedrofurla	11:21	`A <: B`, `F[A] <: F[B]`
haskellandchill	11:21	god no please no
pedrofurla	11:21	`A <: B`, `F[B] <: F[A]`
pedrofurla	11:21	heheh
haskellandchill	11:21	any way if anyone isn't solid on reading haskell type signatures
haskellandchill	11:22	you have an `a`, a `b`, and a `f a`
haskellandchill	11:22	you get an `f b`
katychuang	11:22	i remember it taking a while to learn how to read haskell type signatures 😃
haskellandchill	11:22	thats normal functor
haskellandchill	11:22	you have an `a`, a `b`, and a `f b`
katychuang	11:22	`f a` and `f b` are functions btw
haskellandchill	11:22	you get a `f a`, that's contra
haskellandchill	11:22	`f` is a type level function and `a` is a type
katychuang	11:23	oh right that confused me
pedrofurla	11:23	type constructor, please
m	11:23	:whoosh:
haskellandchill	11:23	`f a` is `f` applied to `a`
haskellandchill	11:23	I prefer the perspective of type level functions
pedrofurla	11:23	a applied to f
pedrofurla	11:23	the arguments are what are applied
haskellandchill	11:23	huh?
pedrofurla	11:24	`f a`, a applied to f
haskellandchill	11:24	we usually say a function is applied to its arguments
haskellandchill	11:24	but either way
pedrofurla	11:24	nopes
haskellandchill	11:24	no problem boss 😉
katychuang	11:25	type constructor = type level functions? is that the conclusion
pedrofurla	11:25	omg, you are right, @haskellandchill https://en.wikipedia.org/wiki/Function_application
haskellandchill	11:25	I know I'm right
haskellandchill	11:25	thanks 🙂
haskellandchill	11:25	a type constructor is a kind of type level function
haskellandchill	11:25	there are others
haskellandchill	11:26	don't need to go into all the type level stuff, it can get complex quick and haskell isn't the best language to express things there
haskellandchill	11:26	key takeaway is you have functions from values to values
haskellandchill	11:27	and also functions from types to types
haskellandchill	11:27	Haskell gives you a very nice lambda calculus for both
haskellandchill	11:28	it's hard for beginners to see where you are working with values, and where you are working with types, but it is crucial to learn the distinction
haskellandchill	11:28	lots of Haskell examples use the same letter for the type and value so it's easy to get confused
haskellandchill	11:29	```
katychuang	11:32	i'm confused again
m	11:32	:whoosh:
haskellandchill	11:43	that just means I failed 😞 best done with a whiteboard
haskellandchill	11:44	`I`
haskellandchill	11:44	those `a`'s mean different things
haskellandchill	11:44	`II`
haskellandchill	11:44	those `f`'s mean different things
haskellandchill	11:45	it is confusing
haskellandchill	11:45	but it is also elegant
haskellandchill	11:45	you need to have the concept of a type judgement
haskellandchill	11:47	in `I` we have judgment `a:a`
haskellandchill	11:47	in `II` we have judgement `a:f a`
haskellandchill	11:47	the `a` before `:` is a value
haskellandchill	11:48	after `:` the `a` is a type
haskellandchill	11:48	`value:type` is a type judgement
m	11:48	i think that makes more sense
sagar	11:50	what are we judging
katychuang	11:50	i don't understand the part where you said “type judgement” - is the compiler making judgements?
sagar	11:51	this is very useful
haskellandchill	11:51	anyone can make a judgement
haskellandchill	11:51	you can do haskell by hand
haskellandchill	11:51	the compiler checks our judgements
haskellandchill	11:51	and infers judgements when we are not explicit
sagar	11:51	oh
haskellandchill	11:51	this is called type checking and type inference, respectively
sagar	11:51	is that like type casting
haskellandchill	11:51	no
sagar	11:51	like implicitly it assumes a type
haskellandchill	11:52	type casting does not exist in Haskell
sagar	11:52	if a type isn't specified (edited)
haskellandchill	11:52	it is unsafe
haskellandchill	11:52	it's inference, not casting
haskellandchill	11:52	you infer a type, then check your inference
haskellandchill	11:52	with casting you force a type from another type
sagar	11:52	ok interesting
sagar	11:52	what's a good 101 on this inference stuff
haskellandchill	11:52	doesn't exist
sagar	11:53	LOL
sagar	11:53	but interesting distinction
haskellandchill	11:53	Proofs and Types
haskellandchill	11:53	but it's more advanced
haskellandchill	11:53	by Jean-Yves Girard, not beginner friendly
sagar	11:53	so - just for mental models sake - inference is like casting except nothing is cast, it is infered and cheked and if the check fails then no compile
haskellandchill	11:53	inference is not like casting
sagar	11:53	where "inference" is the compiler going "oh this variable might be of x type" ?
haskellandchill	11:54	not really
sagar	11:54	hmm ok erases mental blackboard
haskellandchill	11:54	first you say ok it is of type `x`
haskellandchill	11:54	where `x` is a type variable
sagar	11:54	so `int x`
haskellandchill	11:54	then you use unification to constrain the concrete type of type variable `x`
haskellandchill	11:55	unification is a tool from logic
haskellandchill	11:55	you get two sides of an equation
haskellandchill	11:55	for example
haskellandchill	11:55	`Int = x`
haskellandchill	11:55	then you can infer type variable `x` is concrete type `Int`
katychuang	11:56	-- this is how I read it
haskellandchill	11:56	ok thanks @katychuang let me clarify
haskellandchill	11:56	```
katychuang	11:56	aha!
katychuang	11:57	so not exactly haskell syntax just yet
haskellandchill	11:57	I'm talking at a meta level
haskellandchill	11:57	very informally
katychuang	11:57	ahh got it
haskellandchill	11:58	@sager if you want to know more and are comfortable with Haskell syntax I can point you to some examples
haskellandchill	11:58	er @sagar
sagar	11:58	this is great
haskellandchill	11:58	it's fun to work through type constraint unification
haskellandchill	11:58	a few Haskell books have chapters on it that are very instructive
sagar	11:59	i don't think i'm that comfortable yet, i just finished the lambda calculus stuff. I have an undergrad in electronics engineering from over 10 years ago so i'm pretty happy in mathland, programming land not so much unless we're working with PLC's
haskellandchill	11:59	ok, yes learning to hold off on advanced things is key
haskellandchill	11:59	you can't just try and learn everything, it's overwhelming
katychuang	11:59	I feel like I need a brief refresher on unification - where is it from, do mathematicians use it?
haskellandchill	11:59	unification comes from logic, it is the basis of something like Prolog
sagar	12:00	the first chapter of the book took me back to like 11th grade heh functions, domains etc
haskellandchill	12:00	https://en.wikipedia.org/wiki/Unification_(computer_science)
haskellandchill	12:00	wikipedia page is very good
sagar	12:00	when i am better at it - @haskellandchill would you like to collaborate on a 101 medium blog post
haskellandchill	12:00	certainly
sagar	12:00	awesome
haskellandchill	12:01	I was going to edit some of this into “A Conversation About …” something ha
katychuang	12:01	👍 👍
katychuang	12:01	i see a bunch of greek letters on that wikipedia page
haskellandchill	12:01	yup
haskellandchill	12:02	> For example, using x,y,z as variables, the singleton equation set { cons(x,cons(x,nil)) = cons(2,y) } is a syntactic first-order unification problem that has the substitution { x ↦ 2, y ↦ cons(2,nil) } as its only solution. The syntactic first-order unification problem { y = cons(2,y) } has no solution over the set of finite terms; however, it has the single solution { y ↦ cons(2,cons(2,cons(2,...))) } over the set of infinite trees. The semantic first-order unification problem { a⋅x = x⋅a } has each substitution of the form { x ↦ a⋅...⋅a } as a solution in a semigroup, i.e. if (⋅) is considered associative; the same problem, viewed in an abelian group, where (⋅) is considered also commutative, has any substitution at all as a solution. The singleton set { a = y(x) } is a syntactic second-order unification problem, since y is a function variable. One solution is { x ↦ a, y ↦ (identity function) }; another one is { y ↦ (constant function mapping each value to a), x ↦ (any value) }.
sagar	12:02	i didn't know the word ofr it was unification i always called it resolving an expression
sagar	12:02	from high school stuff
haskellandchill	12:02	that's a good section to try and understand, let me know if you have questions
katychuang	12:04	it's a challenge to read. i think in pictures and this is all text
haskellandchill	12:04	yea I want to do visualizations
haskellandchill	12:05	it's ok to accept you can't aren't prepared for the formalism and move on
haskellandchill	12:05	that wikipedia page isn't going anywhere 😄
katychuang	12:05	It's cool that John Alan Robinson came up with the unification algorithm, contributing to foundations of automated theorem proving. That gives some context
katychuang	12:06	Now I see unification is important as far as having a premise that the machine can compute the logic (I assumed it was a given that computers can compute as a millennial)
katychuang	12:06	So yes, moving on 🙂
pedrofurla	12:10	wow, the conversation changed drastically