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

https://developer.mozilla.org/en-US/

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

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

https://developer.mozilla.org/en-US/docs/Learn/Getting_started_with_the_web

it has things like “installing a text editor”

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

it mentions things like ftp

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

maybe jsfiddle instead of notepad.exe

@qqq http://htmldog.com/

that's how i learnt them

there's a companion book too

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

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

nope it was the first thing i learnt

http://www.catb.org/esr/faqs/hacker-howto.html this is what started it for me

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

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

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

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

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

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

@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.

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

this is very vaguish:

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

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

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

@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.

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

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 ?

there's an untyped lambda calculus

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

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

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.

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

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

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

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

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

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

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

you can't make polymorphism using it

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

"dependent" is waay too overloaded in this field.

> 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.

https://en.wikipedia.org/wiki/System_F

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

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

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?

that sounds like a decent description of polymorphism actually

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

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

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.

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

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

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

@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.

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

heh, i'm cheating, going by HoTT https://homotopytypetheory.org/book/

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

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

agreed.

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

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

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

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

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

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

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

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

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

ie a higher order metavar.

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.

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

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

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

http://repository.cmu.edu/cgi/viewcontent.cgi?article=2289&context=compsci

> 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, ...

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

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

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

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

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

"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.

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.

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

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

at least thats what it looks like to me. 😉

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.

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

sorry for the crappy ascii emulation of greek characters

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

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

its syntax all the way down.

that's a type as a parameter

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

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

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

there's no code in this paper

even worse!

downloading paper now

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

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".

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.

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

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

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

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

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

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

it's the simplest corner of the lambda cube

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

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

I want to understand it too

@qqq link http://repository.cmu.edu/cgi/viewcontent.cgi?article=2289&context=compsci

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

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

I heard https://www.cs.uoregon.edu/research/summerschool/archives.html is really good too @noisesmith

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

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

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

@noisesmith : https://www.google.com/search?q=types+and+programming+languages+figure+23-1&source=lnms&tbm=isch

look at the first image

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

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

you might find this useful: https://softwarefoundations.cis.upenn.edu/current/

that appears to only go up to STLC

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

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

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

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

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

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

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