markasoftware 2017-02-09 17:49:02
why is literally everything on the haskell wiki written in such a way that you can't understand it unless you already know it?
monochrom 2017-02-09 17:49:33
ryantm____: Pretty sure you saw the sentence there "You cannot use a deriving clause for a GADT; only for an ordinary data type."
markasoftware 2017-02-09 17:49:36
"The concept of a type family comes from type theory. An indexed type family in type theory is a partial function at the type level. Applying the function to parameters (called type indices) yields a type. Type families permit a program to compute what data constructors it will operate on, rather than having them fixed statically (as with simple type systems) or treated as opaque unknowns (as with parametrically polymorphic types)."
markasoftware 2017-02-09 17:49:41
what the flying fuck does this mean
c_wraith 2017-02-09 17:49:45
markasoftware: It's not. It's written so that if you know haskell, you can learn new concepts.
ryantm____ 2017-02-09 17:50:18
monochrom: You can use standalone deriving or a GADT generally, it doesn't work for Pair. For example, if you comment out Pair it works.
ryantm____ 2017-02-09 17:50:27
for a GADT*
c_wraith 2017-02-09 17:50:27
markasoftware: type families aren't part of base haskell. They're an extension. They only make sense if you know base haskell.
markasoftware 2017-02-09 17:50:35
i mostly know base haskell
markasoftware 2017-02-09 17:50:42
not that well, but enough
c_wraith 2017-02-09 17:51:39
markasoftware: so what's unclear about "applying a type function to parameters yields a type"?
markasoftware 2017-02-09 17:51:52
that sentence is ok
monochrom 2017-02-09 17:51:58
markasoftware: Because of self-selection bias. Someone writing on the haskell wiki is very likely in an enthusiastic high mode such that they want to share you with their excitement and keep talking and not think whether you understand or what order is a good order to explain.
c_wraith 2017-02-09 17:52:05
markasoftware: that's all you need to know, until you get to syntax.
markasoftware 2017-02-09 17:52:14
it's unclear what "Type families permit a program to compute what data constructors it will operate on, rather than having them fixed statically (as with simple type systems) or treated as opaque unknowns (as with parametrically polymorphic types)." means
markasoftware 2017-02-09 17:53:31
well, i hope i figure it out eventually
monochrom 2017-02-09 17:53:54
Read the GHC Users Guide for type family. I learned it there.
c_wraith 2017-02-09 17:53:54
Type families just let you write functions on types.
c_wraith 2017-02-09 17:54:04
and yeah, the User's Guide is actually really good.
monochrom 2017-02-09 17:54:27
Bill Gates's appraisal at the back cover of GHC Users Guide: "If you have read it cover to cover, send me your CV"
monochrom 2017-02-09 17:55:35
I also learned GADTs there. I also learned multiple parameter type class there.
c_wraith 2017-02-09 17:55:56
markasoftware: a type family takes types as arguments. You write type instances which pattern-match on types and produce a type.
ryantm____ 2017-02-09 17:56:00
monochrom: I figured it out! If I remove the (Show a) constraint, it works
c_wraith 2017-02-09 17:56:42
markasoftware: the original paper discusses uses of the feature, if you are looking for them: https://pdfs.semanticscholar.org/8dd2/c7c64451e6dda5d72351ef5c75d091352e05.pdf
c_wraith 2017-02-09 17:57:14
markasoftware: I know, "paper" is often a dirty word, but Simon Peyton Jones is a fantastic author. His papers are all readable because they use code instead of random symbols. :)
markasoftware 2017-02-09 17:57:31
oh, is that the guy who made the "haskell is useless" video?
EvanR 2017-02-09 17:57:52
type families seem to be named after indexed families of types, that is, a mapping from some index type A to types, A -> Type. However the Haskell feature doesn't allow you pick the type A...
markasoftware 2017-02-09 17:58:25
coming from js all this type stuff is new to me
markasoftware 2017-02-09 17:58:31
before its just put anything together and it will work
ezyang 2017-02-09 17:58:35
"not just the video" ;)
monochrom 2017-02-09 17:58:40
type-indexed family of types.
ryantm____ 2017-02-09 17:59:16
ezyang: ha!
Whatishisname 2017-02-09 17:59:48
yo
EvanR 2017-02-09 17:59:52
markasoftware: after using haskell for so long, i seem to recall it the opposite way around. Most stuff i put together in js does NOT work...
markasoftware 2017-02-09 18:00:03
yep, hopefully that's how I'll be thinking in 6 months
Whatishisname 2017-02-09 18:00:07
is this the most popular haskell channel
EvanR 2017-02-09 18:00:07
at least not until some monumental mental efforts
Whatishisname 2017-02-09 18:00:08
?
markasoftware 2017-02-09 18:00:17
Whatishisname: yes
monochrom 2017-02-09 18:00:17
Yes.
markasoftware 2017-02-09 18:00:27
EvanR: is your username based on Yesod resource naming scheme?
Whatishisname 2017-02-09 18:00:28
ok am gonna hang here then
c_wraith 2017-02-09 18:00:50
markasoftware: yes, he is the one from that video. He's also been one of the main authors of GHC for over 20 years. He knows a bit about it. :)
markasoftware 2017-02-09 18:00:55
js is sh*t to debug though
Whatishisname 2017-02-09 18:00:57
I tried doing a crash course on lambda calculus
Whatishisname 2017-02-09 18:01:01
seemed very simple
Whatishisname 2017-02-09 18:01:07
am I missing something?
monochrom 2017-02-09 18:01:08
I learned js after haskell. And everything I put together works. Both side.
EvanR 2017-02-09 18:01:10
my username is actually based on a suggestion by eric S raymond to not use silly names online
Whatishisname 2017-02-09 18:01:27
I learnt Java first
Whatishisname 2017-02-09 18:01:33
now learning JS
monochrom 2017-02-09 18:01:37
I even trampolined correctly in js.
Whatishisname 2017-02-09 18:02:03
JS seems like a confused person to me
markasoftware 2017-02-09 18:02:03
monochrom: what a god
Whatishisname 2017-02-09 18:02:10
it has its hands in everything
markasoftware 2017-02-09 18:02:11
not as bad as php at least
EvanR 2017-02-09 18:02:14
well now that i see imaginary types in js, it works more often
markasoftware 2017-02-09 18:02:36
"5 dogs" == "5.00000000000000000000000000000001" => true in js
markasoftware 2017-02-09 18:02:39
i mean php
markasoftware 2017-02-09 18:02:41
sorry
markasoftware 2017-02-09 18:02:44
definitely not true in js
Whatishisname 2017-02-09 18:02:50
anyone know lambda calculus?
monochrom 2017-02-09 18:03:39
how much do I have to know to qualify as your "know"?
Whatishisname 2017-02-09 18:03:49
that's right
Whatishisname 2017-02-09 18:04:00
the eternally unsure knowledable guy
Whatishisname 2017-02-09 18:04:10
you know enough
monochrom 2017-02-09 18:04:20
I concur.
Whatishisname 2017-02-09 18:04:25
First am consued about how zero is notated
Whatishisname 2017-02-09 18:04:39
then it seems all too simple
Whatishisname 2017-02-09 18:04:47
that I don't know what the fuss is about
Whatishisname 2017-02-09 18:05:01
confused*
EvanR 2017-02-09 18:05:03
LC was an attempt at a formal language for logic, but they messed up and made a programming language instead
monochrom 2017-02-09 18:05:13
haha
Whatishisname 2017-02-09 18:05:22
oh nice nice that explains a bit
dhalgren_ 2017-02-09 18:05:38
what do you expect? what fuss? afaik its supposed to be a minimalist abstract formalism of what an "algorithm" is, analogous to the turing machine
monochrom 2017-02-09 18:05:46
I am not going to address "what the fuss". I don't care.
Whatishisname 2017-02-09 18:06:02
ok then
monochrom 2017-02-09 18:06:04
But if you see that things work out as claimed, you already understand.
Whatishisname 2017-02-09 18:06:40
I don't see any difference
monochrom 2017-02-09 18:06:53
And if you don't see how things work out, I can answer.
Whatishisname 2017-02-09 18:06:59
its the same thing deep down
Whatishisname 2017-02-09 18:07:15
instead of a for loop you got like, some notation
Whatishisname 2017-02-09 18:08:16
brb
EvanR 2017-02-09 18:08:23
:t (\x -> x x) (\x -> x x)
lambdabot 2017-02-09 18:08:25
error:
lambdabot 2017-02-09 18:08:25
• Occurs check: cannot construct the infinite type: t0 ~ t0 -> t
lambdabot 2017-02-09 18:08:25
Expected type: t0 -> t
dhalgren_ 2017-02-09 18:08:34
where do for loop come in? aren't we talking about the 'language' w just lambda abstraction, applicaton and variable
monochrom 2017-02-09 18:09:29
See this is why I won't address "what the fuss". You have already made up your mind. I said "I don't care" because I know that you already don't care.
Whatishisname 2017-02-09 18:10:00
monochrom I got not idea what you are talking about
Whatishisname 2017-02-09 18:10:08
dhalgren um
dhalgren_ 2017-02-09 18:10:48
that's the simple l.c. at least afaik
EvanR 2017-02-09 18:11:08
not simple as in simply typed
monochrom 2017-02-09 18:11:20
dhalgren_: "for loop" comes up because "programming" came up, for better or worse.
Whatishisname 2017-02-09 18:11:35
the 'application' part, isn't that just a for loop?
dhalgren_ 2017-02-09 18:11:44
EvanR: yeah, untyped I guess
nshepperd 2017-02-09 18:12:17
Whatishisname: you mean the "apply the rewriting rules until none of them apply"?
monochrom 2017-02-09 18:12:28
the untyped one hides its difficulty in the denotational semantics (if you want one)
Whatishisname 2017-02-09 18:12:50
nshepperd yeah
Whatishisname 2017-02-09 18:13:25
function application seems like a list iteration
EvanR 2017-02-09 18:13:28
that would be a while loop
Whatishisname 2017-02-09 18:14:05
sure you don't have to work all the details but aren't they both the same thing?
nshepperd 2017-02-09 18:14:09
I don't think that's really a for loop any more than the cpu of a machine carrying out instructions is
nshepperd 2017-02-09 18:14:28
the cpu executes the current execution and advances the IP until it runs out
athan 2017-02-09 18:15:24
If I have a rose tree, but modified to be a zipper, could I use a lens to focus to a specific point?
Whatishisname 2017-02-09 18:15:28
deep down in the CPU all just jumps
nshepperd 2017-02-09 18:15:34
similarly, the LC 'machine' evaluates the current term by applying rewriting rules until it runs out of rules
EvanR 2017-02-09 18:16:08
if it was all just jumps, you could optimize away the cpu entirely
monochrom 2017-02-09 18:16:34
I think this is a pointless discussion.
EvanR 2017-02-09 18:16:35
or replace it with a simple heater, because there would be no observable result of computation
Whatishisname 2017-02-09 18:16:47
yeah but the 'LC' machine does not exist.
athan 2017-02-09 18:17:04
lambdacalculus machine?
athan 2017-02-09 18:17:16
There's an SK combinator chip thing iirc
athan 2017-02-09 18:17:28
(that I really want to have >.> muh supercombinators)
Whatishisname 2017-02-09 18:17:58
you do it with a for loop or a function application, the machine we got does the same thing
dhalgren_ 2017-02-09 18:18:08
I mean, application is just any application of a lambda abstraction to a variable. like where are the implicit for loops in say the Y combinator Y = λ f . ( λ x . f ( x x ) ) ( λ x . f ( x x ) ) ?
nshepperd 2017-02-09 18:18:33
monochrom: quite.
dhalgren_ 2017-02-09 18:19:02
(actually to a lambda term)
Whatishisname 2017-02-09 18:19:32
dhalgren what does the f stand for?
athan 2017-02-09 18:19:36
dhalgren_: iirc you can turn Y into a recursive pointer thing, but not an explicit for loop, because of decidable termination or something
Whatishisname 2017-02-09 18:19:44
is there a faster way to print people's names?
Whatishisname 2017-02-09 18:19:54
like a shortcut?
dhalgren_ 2017-02-09 18:20:28
well its any lambda term, right :)
Whatishisname 2017-02-09 18:21:40
ok the expression you typed, it could be just a sequence of instructions.
Whatishisname 2017-02-09 18:21:50
the loop happens when you supply it an input
Whatishisname 2017-02-09 18:21:57
function application?
EvanR 2017-02-09 18:22:17
so you want to implement lambda calculus with C
monochrom 2017-02-09 18:22:38
No, C is too complex. Use BASIC.
dhalgren_ 2017-02-09 18:22:47
well obviously, given that turing machines and lambda calculus are proved to be equivalent. There's a few other formalisms that are equivalent to it too
Whatishisname 2017-02-09 18:22:55
fortunaltely i know just BASIC :D
Whatishisname 2017-02-09 18:23:17
It has a GOSB
Whatishisname 2017-02-09 18:23:21
GOSUB
Whatishisname 2017-02-09 18:23:50
my point is if you pay attention to what is happening deep down, you see no difference between the two styles
Whatishisname 2017-02-09 18:24:15
What is the point of having a different style?
EvanR 2017-02-09 18:24:22
next you will challenge us to prove you wrong
Whatishisname 2017-02-09 18:24:33
How is that?
EvanR 2017-02-09 18:24:39
just a guess
Whatishisname 2017-02-09 18:25:03
ok
Whatishisname 2017-02-09 18:25:27
tell me what benefit is there to programming this way if you know what is happening deep down
EvanR 2017-02-09 18:26:34
no one programs that way
Whatishisname 2017-02-09 18:26:41
dhalgren oh so they are equivalent
Whatishisname 2017-02-09 18:27:03
so its all just semantics
Whatishisname 2017-02-09 18:27:06
then?
EvanR 2017-02-09 18:27:24
by default LC doesnt even come with semantics
EvanR 2017-02-09 18:27:32
its meaningless!
Whatishisname 2017-02-09 18:27:46
:D
dhalgren_ 2017-02-09 18:27:51
Whatishisname: basically 4 mathematicians in about the same time were solving the same problem. 2 together and the other 2 each independently solved it with a formalism of their own. Turing created the turing machine, Church created the lambda calculus, and Godel and Herbrand general recursive functions. THen they proved they are all equivalent.
Whatishisname 2017-02-09 18:28:19
dhalgren oh I did not know
Whatishisname 2017-02-09 18:28:33
I though LC was this special new something
Whatishisname 2017-02-09 18:28:35
:D
dhalgren_ 2017-02-09 18:28:47
this was in the early 1930s. :)
EvanR 2017-02-09 18:29:24
LC is almost 90 years old, and Begriffsschrift is even older
Whatishisname 2017-02-09 18:29:42
ok what else can you do with this style. other than having shorter code?(coz of the implicit loops)
EvanR 2017-02-09 18:29:45
and calculus ratiocinator is even older
Whatishisname 2017-02-09 18:30:13
what is that?
Whatishisname 2017-02-09 18:30:40
dhalgren what was the problem they were trying to solver?
Whatishisname 2017-02-09 18:30:46
solve*
Whatishisname_ 2017-02-09 18:33:15
I got dced
Whatishisname_ 2017-02-09 18:33:31
I work with a group of people who don't see the point of say OOP, patterns etc
Whatishisname_ 2017-02-09 18:33:40
Its all a rearrangement of code to them
Whatishisname_ 2017-02-09 18:33:54
and unecessarily complicating things
dhalgren_ 2017-02-09 18:34:12
formalizing what a "computable function" really is; basically showing that if a human could calculate something, at least given infinite resources and time, then so could a turing machine/lambda expression etc.
Whatishisname_ 2017-02-09 18:34:23
it is much easier to manually fix everything than any benefit those things provide
Whatishisname_ 2017-02-09 18:34:50
ok the idea of what is 'computable'
EvanR 2017-02-09 18:34:51
not a human
monochrom 2017-02-09 18:35:18
I don't see the point of OOP either.
EvanR 2017-02-09 18:35:47
if an "idealized mathematician", one who only carries out a fixed algorithm, who can follow the instructions exactly without messing up, but ultimately unable to do any "genuine reasoning" of his own
EvanR 2017-02-09 18:35:56
could do it, so could a turing machine
monochrom 2017-02-09 18:36:34
I do see the point of patterns. They mean the language you chose is too dumb to make your boilerplate a procedure, so you have to keep writing the boilerplate and you call it a pattern to feel better.
Whatishisname_ 2017-02-09 18:36:34
so the idea of which task does not involve any thinging other than calculations
Whatishisname_ 2017-02-09 18:36:41
thinking*
dhalgren_ 2017-02-09 18:36:43
yes, a human following an algorithm, sry
monochrom 2017-02-09 18:37:25
You can see more past computers in the movie HIdden Figures.
dhalgren_ 2017-02-09 18:37:26
I should really stop talking mathematics in a room with matematicians present, my sloppiness is bound to irritate :D
Whatishisname_ 2017-02-09 18:37:28
A machine can do add. that's about it
EvanR 2017-02-09 18:37:32
a human may be able to make progress enumerating busy beaver numbers, but we now know a computer cant
Whatishisname_ 2017-02-09 18:37:37
everything is else is derived off that
monochrom 2017-02-09 18:37:45
And you will see that they will learn programming too.
Whatishisname_ 2017-02-09 18:37:50
wait also read and write to a storage
EvanR 2017-02-09 18:38:51
hmm, maybe a computer can
Whatishisname_ 2017-02-09 18:38:54
off of reading and writing to storage, you get registers
monochrom 2017-02-09 18:38:54
@quote monochrom substitut
lambdabot 2017-02-09 18:38:54
monochrom says: Dilbert's substitutability principle. A subclass's programmer should work as a drop-in replacement of his/her predecessor.
EvanR 2017-02-09 18:38:56
but not an algorithm
Whatishisname_ 2017-02-09 18:39:22
if you make the location of read write variable then you get an index register
Whatishisname_ 2017-02-09 18:39:33
you get sequential computing
Whatishisname_ 2017-02-09 18:39:34
jumps
Whatishisname_ 2017-02-09 18:39:51
hmm what would be an if statement
Whatishisname_ 2017-02-09 18:39:58
a comparision
EvanR 2017-02-09 18:40:09
none of this pertains to haskell
EvanR 2017-02-09 18:40:26
im here to kick ass and do haskell
Whatishisname_ 2017-02-09 18:40:27
it pertains to computers
Whatishisname_ 2017-02-09 18:40:29
:D
Whatishisname_ 2017-02-09 18:40:41
and what is computable
EvanR 2017-02-09 18:40:56
ideally in haskell
monochrom 2017-02-09 18:40:58
Clearly the foundation of computing is important to a Haskell channel.
Whatishisname_ 2017-02-09 18:41:01
Am trying to figure out the point of what the mathematicians did
monochrom 2017-02-09 18:41:17
Next you're going to learn quantum mechanics with me because it's how computers work.
Whatishisname_ 2017-02-09 18:41:20
what was the point of LC or turing machine
Whatishisname_ 2017-02-09 18:41:26
it seems so straight forward
Whatishisname_ 2017-02-09 18:41:29
:(
EvanR 2017-02-09 18:41:44
i have a few books here which go into the point
glguy 2017-02-09 18:41:48
Sorry Whatishisname_, the topic of this channel is *specifically* Haskell programming rather than anything related to computers
EvanR 2017-02-09 18:41:52
blurbs dont do it justice
monochrom 2017-02-09 18:41:58
Yes quantum mechanics is straightforward and obvious too. At least according to Scott Anderson.
Whatishisname_ 2017-02-09 18:41:58
maybe at that time they had no concrete proof of anything
EvanR 2017-02-09 18:42:16
you are pretty close
Whatishisname_ 2017-02-09 18:42:25
how about the point of lambda calculus?
Whatishisname_ 2017-02-09 18:42:31
glguy
Whatishisname_ 2017-02-09 18:42:35
I wills top spamming
EvanR 2017-02-09 18:42:56
in the late 19th century peano was famous for publishing mathematical works where each step in the "proof" merely looked like the previous step
Whatishisname_ 2017-02-09 18:42:56
you see to a guy here it is very hard to explain this
EvanR 2017-02-09 18:43:21
no basis for how you get from one step to the other was given in most of his work
EvanR 2017-02-09 18:44:25
up to that point mathematical proofs consisted of a lot more "intuitive" reasoning, rather than what we now consider logic
Whatishisname_ 2017-02-09 18:44:30
so we need proofs for...
monochrom 2017-02-09 18:44:50
me
Whatishisname_ 2017-02-09 18:44:57
peano was it?
monochrom 2017-02-09 18:44:58
I demand proof.
EvanR 2017-02-09 18:45:00
frege said fuck that, but was larely unknown until the 1920s
