This page is not created by, affiliated with, or supported by Slack Technologies, Inc.
- # bangalore-clj (1)
- # beginners (99)
- # boot (108)
- # cider (15)
- # clara (4)
- # cljs-dev (12)
- # cljsjs (37)
- # cljsrn (4)
- # clojure (110)
- # clojure-italy (2)
- # clojure-spec (12)
- # clojurescript (168)
- # cursive (1)
- # datomic (24)
- # graphql (6)
- # hoplon (5)
- # jobs-discuss (2)
- # keechma (21)
- # mount (5)
- # off-topic (140)
- # om (2)
- # parinfer (37)
- # planck (6)
- # re-frame (4)
- # reagent (9)
- # rum (2)
- # spacemacs (4)
MDN has beginner level stuff, and their info is a lot better than most stuff that’s supposedly good for beginners
I think that's pretty hard to grasp unless there's someone sitting ext to you and tutoring you
the absolute simplest might be something like a youtube video of someone typing in notepad.exe, and you copy them step by step
@sundarj : that site is ad infested 🙂 // did you know programming already when you started html/css/js ?
yes, I know how to use ublock origin, but this is meant for someone starting to leran programming
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
@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 think for newcomers, 'immediate feedback / seeing something working / building a small demo' is really important to keep people motivated
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.
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 ?
seems to say "values depending on types" is what separates systemF from stlc
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.
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
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
> 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.
ah "values depending on types" really means "variables whose value 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?
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
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
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
is there even a distinction at this level in this abstraction? it seems like there isn't any
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.
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.
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
> 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
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.
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
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
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.
we use semantics to make sure our syntax is "good". once we have the syntax we (like computers) no longer need semantics.
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
so in types and programming langages, chapter 23, there's an image which shows the eval / typing rules of stlc
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/
@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.
learn coq and you deepen your understanding of all programming language. so i imagine.