wingsorc has quit [Remote host closed the connection]
Guest1409 is now known as Ankhers
MarvelousWololo has joined #ocaml
waleee has quit [Ping timeout: 264 seconds]
tomku has quit [Ping timeout: 250 seconds]
tomku has joined #ocaml
aljazmc has quit [Remote host closed the connection]
perrierjouet has joined #ocaml
<discocaml>
<contificate> I'd recommend Appel's other series of books, Modern Compiler Implementation in ML (or C, or two editions in Java).
end^ has joined #ocaml
lobo[m] has joined #ocaml
reynir[m] has joined #ocaml
zebrag[m] has joined #ocaml
jmcantrell has joined #ocaml
MuqiuHan[m] has joined #ocaml
<discocaml>
<contificate> Not that CwC doesn't have valuable treatment of certain topics, it's just you'd probably never faithfully lower down such a representation (as it implies a custom back-end, practically) and, to some extent, it's more of a non-beginner's pamphlet about the design of SMLNJ.
bgs has quit [Remote host closed the connection]
John_Ivan_ has quit [Ping timeout: 244 seconds]
kitzman has quit [Quit: C-x C-c]
kitzman has joined #ocaml
perrierjouet has quit [Quit: WeeChat 4.0.2]
perrierjouet has joined #ocaml
Anarchos has joined #ocaml
Serpent7776 has joined #ocaml
bartholin has quit [Ping timeout: 246 seconds]
bartholin has joined #ocaml
Anarchos has quit [Ping timeout: 245 seconds]
Anarchos has joined #ocaml
John_Ivan has joined #ocaml
perrierjouet has quit [Quit: WeeChat 4.0.2]
perrierjouet has joined #ocaml
bartholin has quit [Quit: Leaving]
<darchitect>
hey guys, can someone please explain how type theory relates to the study of programming language design in laymen's terms, I think I've got a rough idea by now, but I would like to get more people's oppinions on it (i.e. more oppinions about how to best summarise the relationships between type theory and functional programming languages)
<discocaml>
<contificate> I think the way Benjamin C. Pierce phrases it in the start of TAPL is apt.
<discocaml>
<contificate> > A type system is a tractable syntactic method for proving the absence of
<discocaml>
<contificate> > certain program behaviors by classifying phrases according to the kinds
<discocaml>
<contificate> > of values they compute.
<darchitect>
neat !@
<darchitect>
what is TAPL ?
<discocaml>
<contificate> If you're getting started, I recommend starting small. Can look at things like the Curry-Howard correspondence as it relates simple systems, like propositional logic and simply typed lambda calculus.
<discocaml>
<contificate> TAPL is Pierce's book "Types and Programming Languages"
<darchitect>
but I want to get deeper into the theory ...
<darchitect>
would you recommend starting with TAPL or with PFPL (Harper)
<darchitect>
?
<discocaml>
<contificate> If you want stronger theory, I recommend "Type Theory and Formal Proof". If you're a beginner beginner, TAPL is ideal.
<discocaml>
<contificate> I think Harper is good but it's kind of _different_, everything in the book is Bob Harper'd in its exposition, if I recall correctly. Still a good book, and was recommended at my university.
<discocaml>
<contificate> Practically speaking though, I believe earlier you said you wanted to implement a compiler/interpreter for a typed functional language in OCaml?
<darchitect>
well I can code in both languages, but I still can't get throgh Edward Kmett's live coding streams without saying WTF at least 5 times in 1 minute :/
<darchitect>
yeah I do !
<discocaml>
<contificate> Yeah, so you can basically speedrun it.
<discocaml>
<contificate> You would start by looking at simply typed lambda calculus and how its type system has a correspondence with propositional logic. Then, how to implement typechecking? You really just want a unification algorithm.
<darchitect>
what is a unification algorithm ?
<discocaml>
<contificate> (first-order) unification is basically trying to find "unifying" substitutions between two terms to make them equal
<discocaml>
<contificate> so, this is important in polymorphic typechecking because you'll have types that have "unknowns" (type variables)
<discocaml>
<contificate> and you'll need to be able to unify types together to work out which subterms ought to reflect/be the other subterm in the other term
<discocaml>
<contificate> i.e. `Arrow('a, int)` and `Arrow(int, int)` have unifying substitution, `'a => int`
<darchitect>
is type checking implemented manually for every type ?
<discocaml>
<contificate> it does involve case analysis over type terms
<darchitect>
that must be a huge case analysis
<darchitect>
or is it simpler
<discocaml>
<contificate> it's simpler
<discocaml>
<contificate> the rules for typechecking something like simply typed lambda calculus are incredibly straightforward
<darchitect>
oh so it's about decomposing everything into typed lc ?
<discocaml>
<contificate> since the constraints that you collect during the algorithm are easy to express and globally propagate with destructive unification
<discocaml>
<contificate> no, stlc is just a very simple type system to implement
<discocaml>
<contificate> type systems have different properties which make them attractive (or not) - decidability, principality of inference, etc.
<darchitect>
right it makes sense ..
<darchitect>
and as part of language implementation we implement the constraints by case analysis?
<discocaml>
<contificate> helps if you can read inference rules, as, when read bottom to top, they kind of mirror how many inference algorithms are shaped/implemented
<discocaml>
<contificate> well, there's implicit constraints right which are captured by unification patterns
<discocaml>
<contificate> for example, if you're typechecking `f x`, i.e. `App(f, x)` for some `f` and `x` (both lambda terms/expressions)
<discocaml>
<contificate> you know that no matter what, `f` must have an arrow type (`x -> y` for some `x` and `y`)
<darchitect>
true
<discocaml>
<contificate> and you know that its domain type must match that of what it's being applied to
<darchitect>
what is a domain type ?
<discocaml>
<contificate> if a function is an arrow `X -> Y`, then `domain(f)` = `X`
<darchitect>
oh right yeah
<darchitect>
(y)
<discocaml>
<contificate> so this is like trivial in many cases, and captured wholly by how we unify out the application's type
<darchitect>
yeah then the rule makes sense
<darchitect>
can you point me to an example implementation of simply typed lambda calculus (or even untyped lambda calculus) (as in github repo) ?
<discocaml>
<contificate> ```ocaml
<discocaml>
<contificate> App (f, x) ->
<darchitect>
I would like to read through the code to get more understanding
<discocaml>
<contificate> let f_ty = infer env f in
<discocaml>
<contificate> let x_ty = infer env x in
<discocaml>
<contificate> let r_ty = fresh_type_variable () in
<discocaml>
<contificate> infer f_ty (Arrow (x_ty, r_ty)); (* captures case that f must be another Arrow to be unified against an Arrow *)
<discocaml>
<contificate> r_ty
<discocaml>
<contificate> ```
<discocaml>
<contificate> ```ocaml
<discocaml>
<contificate> App (f, x) ->
<discocaml>
<contificate> let f_ty = infer env f in
<discocaml>
<contificate> let x_ty = infer env x in
<discocaml>
<contificate> let r_ty = fresh_type_variable () in
<discocaml>
<contificate> unify f_ty (Arrow (x_ty, r_ty)); (* captures case that f must be another Arrow to be unified against an Arrow *)
<discocaml>
<contificate> r_ty
<discocaml>
<contificate> ```
<discocaml>
<contificate> sorry, I meant to call `unify` in that snippet
<discocaml>
<contificate> anyway, we prolly misusing this channel
<darchitect>
hahah yeah
<darchitect>
thanks anyway
<darchitect>
I will look into the example
<discocaml>
<contificate> no worries, if you understand first-order unification as a concept and why it's used
<discocaml>
<contificate> sound_eager is for a subset of Hindley-Milner though, but you can easily simplify it out to be an STLC impl, which just wouldn't have a generalisation or instantiation
<discocaml>
<contificate> can find other treatment of what's presented in sound_eager in (French) 'Le Language Caml' or 'Functional Approach to Programming'
<darchitect>
thanks !!
Serpent7776 has quit [Ping timeout: 240 seconds]
azimut has quit [Remote host closed the connection]
azimut has joined #ocaml
Tuplanolla has quit [Quit: Leaving.]
Anarchos has quit [Quit: Vision[]: i've been blurred!]