Fork me on GitHub
#off-topic
<
2017-08-05
>
noisesmith00:08:48

mozilla’s MDN has great docs for HTML, CSS, JS, etc.

qqq00:08:43

I should clarify, I'm looking for resources for someone who has never programmed before

noisesmith00:08:11

MDN has beginner level stuff, and their info is a lot better than most stuff that’s supposedly good for beginners

noisesmith00:08:19

it has things like “installing a text editor”

qqq00:08:23

I think that's pretty hard to grasp unless there's someone sitting ext to you and tutoring you

qqq00:08:33

it mentions things like ftp

qqq00:08:01

the absolute simplest might be something like a youtube video of someone typing in notepad.exe, and you copy them step by step

qqq00:08:06

maybe jsfiddle instead of notepad.exe

sundarj02:08:36

that's how i learnt them

sundarj02:08:45

there's a companion book too

sundarj02:08:52

(it has/d the esr seal of approval to boot)

qqq02:08:03

@sundarj : that site is ad infested 🙂 // did you know programming already when you started html/css/js ?

qqq12:08:35

yes, I know how to use ublock origin, but this is meant for someone starting to leran programming

sundarj02:08:19

nope it was the first thing i learnt

varunited11:08:16

@qqq a good book to start with: http://eloquentjavascript.net Has three parts: language, browser and node.

qqq12:08:38

in learning type systems / writing type checkers, how does support for "Union types" work? i.e. type Shape = Rect width height | Square side | Circle radius

hmaurer12:08:29

Objects carry along a tag indicating which types they belong to

fedreg14:08:03

Easier to read it at http://elm-lang.org/examples/buttons but note the extra styling in the snippet

qqq15:08:38

@fedreg : it's a far superior language too, though I'm not sure if 'typed' or 'untyped' is a better first langauge

qqq15:08:49

static type errors can be confusing without a background using static types

qqq15:08:14

my first languages were: c (failed), q basic, c, scheme

fedreg15:08:55

@qqq If you use Elm mainly for its 'view' function and keep the model minimal then i think it is a good way to learn HTML/CSS without worrying too much about typing. The fact that the DOM is checked by the compiler makes it really helpful for learning HTML.

fedreg15:08:21

I also started with BASIC and C. Wish Elm was around when I was a kid!

qqq15:08:37

this is very vaguish:

qqq15:08:01

I think for newcomers, 'immediate feedback / seeing something working / building a small demo' is really important to keep people motivated

qqq15:08:14

jsfiddle / elm's ide does provide this to some extent

qqq15:08:40

but being able to build a full fledge minimal app (html + js + react + sql backend) all from a single ide, with a single set of tutorials, that'd be really instructive

fedreg15:08:01

@qqq Sure. I guess for me html + js + react + sql would be a lot to digest in one tutorial so I'd rather learn how to get something on the screen first, style it, make it interactive, and then worry about everything else once I can do that. But of course it depends on the individual and how comfortable they are with complexity.

fedreg15:08:57

But yes, a course that went through all that in a nice order would be helpful.

qqq18:08:22

in systemF, what does "values depending on types" mean? https://en.wikipedia.org/wiki/Lambda_cube don't values always depend on types, even in basic simply-typ;ed-lambda-calculus ?

noisesmith18:08:30

there's an untyped lambda calculus

noisesmith18:08:02

in fact, "lambda calculus" without modifier usually indicates the untyped kind

qqq18:08:10

the lambda cube starts with "stlc" (in the diagram)

qqq18:08:29

the quote

Values depending on types, or polymorphism. System F, aka second order lambda calculus (written as λ2 in the diagram), is obtained by imposing only this property.
seems to say "values depending on types" is what separates systemF from stlc

noisesmith18:08:51

right, you aren't simply typed any more if you have polymorphism

qqq18:08:18

so my question is -- what does "values depending n types" mean? even in stlc, doesn't values depend on types ?

noisesmith18:08:37

I guess saying having only one type constructor and no polymorphism means "values don't depend on types" is weird

qqq18:08:19

only one type constructor? don't you still have tuples / pairs / records in stlc? or am I wrong in that regard?

noisesmith18:08:38

reading - the key might by that polymorphism can't be defined using -> but the types in stlc can

qqq18:08:09

hmm; the reason I ask this is that the cube has 3 dimensions

noisesmith18:08:16

you can make things that act like those using only the one constructor

noisesmith18:08:31

you can't make polymorphism using it

qqq18:08:40

apparently these dims are: values depending on types types depending on types types depending on values so it's really important to get what these three phrases mean

mobileink18:08:27

"dependent" is waay too overloaded in this field.

noisesmith18:08:52

> Whereas simply typed lambda calculus has variables ranging over functions, and binders for them, System F additionally has variables ranging over types, and binders for them.

qqq18:08:00

ah "values depending on types" really means "variables whose value is a type instead of a value" ?

qqq18:08:17

err, "variable whose content is a type instead of a value" ?

noisesmith19:08:06

so maybe it's that it introduces situations where the type of the arg is a variable - that is, you don't know ahead of time which type it has?

noisesmith19:08:30

that sounds like a decent description of polymorphism actually

mobileink19:08:39

i.e. "list of ints" as a var value?

qqq19:08:03

my current understanding is: in stlc: var x = 1 var x = "hello world" var x = int // NOT OKAY in systemF: var x = int // totally fine var y = (list x) // totally fine too, y = (list int) var (z :of-type y) = [1, 2 3] // we're cool with this too, as z is a list of int, and that's what 'y' is

mobileink19:08:24

seems ok my take: simple types: types are not parameterized parametric polymorphism : types parameterized by types ("type-dependent types") dependent types : types parameterized by (non-type, 1st order) values ("value-dependent types') but since types can be values once you move beyond simple types, the only way to keep things straight is to talk in terms of orders or degrees. you could have types dependent on dependent types, etc, ad infinitum. an infinite stack.

noisesmith19:08:34

I think that description of parametric polymorphism is wrong - something that takes an int or a char isn't defining a new "int or char" type that is paramaterized, it effectively has a type variable in its definition, filled by the actual type used when calling

noisesmith19:08:40

or at least that's how I'm reading this stuff

qqq19:08:32

is there a place to just view the evaluation + typing rules of the initial four forms of the lambda cube?

mobileink19:08:17

@noisesmith yeah. i think "values depending on types" is unenlightening. all typed values depend on types, so this is true of simply typed systems too. maybe "values depending on types parameterized by types" which preserves the distinction from type constructors like (Int x String) - the pair type ctor, which is primitive.

noisesmith19:08:16

it's primitive? I'll admit I can't parse all of the wikipedia page for System F, but it definitely doesn't describe pairs as a primitive

noisesmith19:08:57

OK - what I'm reading here says that what System F has that stlc doesn't is a variable that can hold a type

noisesmith19:08:06

which means in practice that a function can have an unknown term which is a type, this is the most primitive thing that can introduce polymorphism it seems like

mobileink19:08:36

well, a type ctor. not sure if that counts as a fn.

mobileink19:08:13

e.g. List(T) where T is of type Type

noisesmith19:08:18

is there even a distinction at this level in this abstraction? it seems like there isn't any

noisesmith19:08:36

this is quite a few steps before there's any such thing as List

noisesmith19:08:16

(if I'm understanding this stuff correctly, I'm no expert)

mobileink19:08:30

there is in type theory, but i admit lambda calc != type theory.

noisesmith19:08:16

what we have is functions, which when supplied with bindings produce some result, those bindings can be called variables. in System F, it seems like the thing introduced is that the binding can hold a type

mobileink19:08:24

eg type Nat is defined inductively by two ctors Z (zero) and S (succesor). S is not a fn.

mobileink19:08:21

"binding can hold a type" => "fn defn can have an arg of type Type"?

mobileink19:08:37

ie a higher order metavar.

noisesmith19:08:55

if I comprehend what I'm reading, that's what's being described here > Whereas simply typed lambda calculus has variables ranging over functions, and binders for them, System F additionally has variables ranging over types, and binders for them.

mobileink19:08:47

still sounds slightly off to me. what's a "binder"? for-all?

mobileink19:08:29

there's a terminological issue too. "ranging over x" =? "of type x"?

noisesmith19:08:56

so I skipped from wikipedia to one of the papers it references, and this seems more clear - but I can't copy paste the text

noisesmith19:08:18

> It is evident that the meaning of such expressions depend upon both their free normal variables and their free type variables ... For example ... the polymorphic identity function, which maps t to the identify function for objects of type t, ...

noisesmith19:08:10

it seems certain at this point that difference between stlc and system f is that it can put a type in a variable

noisesmith19:08:59

if you are bootstrapping polymorphism, it makes sense for a polymorphic identity to be a an early step, cool

mobileink20:08:09

yeah. it's syntactic. you add a new class of (meta) symbols.

noisesmith20:08:35

I don't even know what something being syntactic means in this system

noisesmith20:08:50

we have objects and rewriting rules and symbols - do you mean it's just adding symbols?

mobileink20:08:47

"normal" variables can only "refer" to simple vals of the right type - that's a syntactic constraint. "type" vars can refer to type vals, again syntactic.

mobileink20:08:52

e.g. List(a), where a is a type param. that must be fixed syntactically in the lang design, e.g. "lower case syms are type vars" or some such.

mobileink20:08:55

then "List(Int)" is syntactically correct since Int is a type sym.

mobileink20:08:06

so we're extending the language by adding new sym (and meta sym) classes.

mobileink20:08:34

at least thats what it looks like to me. 😉

mobileink20:08:30

every symbol is syntactically constrained by its type. the reason 2+"foo" fails is not because it is semantically nutty but because it violates syntactic rules determined by the types of its constituents.

noisesmith20:08:37

so what's being introduced here is /\ (uppercase \) and it takes a type instead of a function, those are the kinds of things that exist

noisesmith20:08:50

sorry for the crappy ascii emulation of greek characters

mobileink20:08:48

it takes a type var or symbol. a type is something else.

noisesmith20:08:30

> it maps t into the identity function for objects of type t

mobileink20:08:31

its syntax all the way down.

noisesmith20:08:41

that's a type as a parameter

noisesmith20:08:35

this paper isn't making any of this symbol vs. thing distinction you talk about - or at least not in any way I can recognize

mobileink20:08:46

senantically, yes. but computers don't so semantics.

noisesmith20:08:05

this isn't a computer, it's a formal language

noisesmith20:08:15

there's no code in this paper

mobileink20:08:53

downloading paper now

noisesmith20:08:55

OK - if I skip ahead it does introduce syntax formally, but the provision of a type as an arg isn't "just a syntax" - it literally is a type as an argument to a function, in this formal language

mobileink20:08:32

that cannot be the case. formal languages are first of all syntax - that's what "formal" means. in the paper this is implict - it's about semantics, and assumes the syntax is understood. key phrase is in para 2: "syntactically valid program".

mobileink20:08:27

look at his use of "t" for a type. "the type t" really means "the type denoted by the type symbol 't'". t's being a type sym means it can only be used where the syntax allows a type sym.

noisesmith20:08:13

why is the distinction you are adding useful - what does it add that is missing in this paper?

noisesmith20:08:08

the proposal of starting with syntax, before coming up with goals or rules, seems very strange to me

mobileink20:08:14

original q was about lambda cube. thinking about it in terms of syntactic extension seems very natural and simple to me.

mobileink20:08:14

but syntax is rules. goals, i don't know, what goals?

mobileink20:08:21

we use semantics to make sure our syntax is "good". once we have the syntax we (like computers) no longer need semantics.

noisesmith20:08:11

this paper is the one that introduced polymorphism to the lambda calculus

noisesmith20:08:21

it's the simplest corner of the lambda cube

qqq20:08:44

(checks back some time later) -- #offtopic is liked a perpetual motion machine 🙂

noisesmith20:08:46

so qqq got me curious, and now I'm trying to understand the thing on its terms

qqq20:08:59

I want to understand it too

mobileink20:08:23

ps. that's why it's called the lambda calulus.

noisesmith20:08:21

I've just been looking at your initial question - what separates System F from stlc - and I have to admit that hasn't /felt/ simple

qqq20:08:58

@noisesmith : there's 1 image that makes systemf vs stlc simple, give me 1 sec

qqq20:08:34

so in types and programming langages, chapter 23, there's an image which shows the eval / typing rules of stlc

qqq20:08:46

err, of systemF, and going from stlc -> systemF is just adding 4 rules

qqq20:08:10

look at the first image

qqq20:08:31

white bg boxes = stlc, grey bg boxes = systemF ^-- this is to the best of my knowledge

qqq20:08:17

so I think there should be similar rules that leads us to all the nodes of the cube, and I'd love to find all these rules

qqq20:08:37

that appears to only go up to STLC

mobileink20:08:27

there's a chapter on ploymorphism and higher-order fns.

qqq22:08:11

@mobileink : is that using/defining polymorphic functions in Coq, or is that about type checking polymorphic functions?

mobileink23:08:12

it's not an implementation guide of that's what you mean. just read it, it's not very long.

mobileink23:08:51

afaik coq is where the badasses go to turn the theory into practice.

mobileink23:08:34

there are others like agda but coq seems to be the fav.

mobileink23:08:16

learn coq and you deepen your understanding of all programming language. so i imagine.

mobileink23:08:59

(just started rewatching The Matrix. Pretty sure it must be coded in a calc-of constructions language. js just would not do.)