<lispy>
schlick: not sure what type of reference you want
<lispy>
schlick: i guess you could mean math functions in ocaml. i think...i saw a list somewhere...
<schlick>
lispy: No, I'm trying to figure out "what does the little crosshairs looking thing mean". That sort of thing. :P
<KrispyKringle>
Exclusive or?
lightstep has quit [Read error: 113 (No route to host)]
<KrispyKringle>
Isn't it?
<pango>
aren't those symbols often overloaded anyway
<schlick>
I don't recall. I have run into one I've never seen before. Something that looks like a capitolized hollow (i.e. just the outline of) N.
<KrispyKringle>
Oh. Hmm. Natural numbers?
<schlick>
That could be.
<schlick>
Just me trying to wade through more stuff on types.
<KrispyKringle>
Yeah. wish I could give you a general help resource, though.
<schlick>
I feel sort of dumb but my concept of types is "how big do I have to make this to stuff something into". Something you had to worry about in C and C++ and not most other languages. :P
<schlick>
I'll have to hit my head against it some more before it sinks in. OO was the same way coming from the basic-with-line-numbers and C and assembly. Only back then it sounded more like hippies on acid talking "You just need more uberhyperpolyfrozle overloading to take care of that man!" instead of remnants of a alien civilization to decode the heiroglyphics of. :P
<schlick>
Basically a plain english description of "well, you remember how they showed you goto encouraged you to write spagette code, and it was a good idea to group things into functions? well, this just groups the data with the functions that work on it" would have sufficed. I haven't figured the basic idea out behind types, though there's some scary looking math-oid stuff on Wikipedia.
<schlick>
though there's some scary looking math-oid stuff on Wikipedia. So far it sorta looks like specifying the set of values something can have, mixed in with the kind of operations you're allowed to do on something, but I can tell that's too simple already, since apparently it can check more than that.
<pango>
the concept isn't that complex... What matters next is what types your language comes with, or allows you to build
<schlick>
pango: What's the basic idea then?
<lispy>
so if you write a function which takes a parameter and adds 1 to it, what would you expect the parameter to be?
<pango>
I agree with your description, allowed values and operations
<lispy>
that's the basic idea behind type inference
<pango>
type is like units in physics, you know something is wrong when you come up with an expression where you add volts with kelvins
<pango>
;)
batdog|gone is now known as batdog
<schlick>
pango: Types seem to be able to check relations between values and stranger things though.
batdog is now known as batdog|gone
<pango>
schlick: I don't think there's a bound zoo of types
<schlick>
Thankfully there doesn't seem to be the proliferation of silly sounding buzzwords with types, but I'm still having trouble figuring out what unifies the whole idea. The closest thing I've seen is the wad of math-ish (they don't have symbols I'm used to seeing) formulas on Wikipedia.
<schlick>
I guess I'll just have to flail at it more till I "get it".
<lispy>
schlick: well, there is typed lambda calculus and system F
<schlick>
lambda calculus I've heard of. "system F" is a new one on me.
<lispy>
both of those explain how it's "held together"
<lispy>
system F is the formal system behind haskell and maybe ML too
<schlick>
lispy: It's probably what the math formulas refer to on Wikipedia then.
<schlick>
Wish there was some reference for those symbols. Unfortunatly, since they aren't "in english" you can't exactly type them into google. "What's the sorta tentaclie looking E-like thing." No results. :P
<lispy>
element of?
<schlick>
Could be.
<schlick>
I have a lot of windows open. Let me see if I can dig up one of the pages that had me glazing over.
<schlick>
Let's see if I can find it by looking up stuff on types again. I think it might have been on the dependent types page, or on one other type theory page.
<schlick>
Ok, the dependent types page was the one with the hollow letters I'd never seen before.
<lispy>
schlick: the 3 bar equal sign means represents equivalence. Which usually requires the author to specify what the "equvalence relation" is
<lispy>
in general, an equivalence relation has 3 properties
<lispy>
if R is the equivalence relation then 1) it's reflexive, x R x, 2) symmetric if x R y then y R x and 3) it's transitive if x R y and y R z then x R z
exa_ has quit [Remote closed the connection]
<lispy>
if some thing R has those three properties you're in bussiness
<lispy>
for example, equals has those properties
<lispy>
but, less than is not an equvalence relation because it doesn't have (2)
<lispy>
1 < 2, but 2 is not less than 1
<schlick>
Heh. I can see vaguely how that would relate to at least functional programming. In the algebraic sense. For some reason I can't remember what reflexive is. I remember transitive from basic algebra and I gather symmetric means that basically it's reversable? Doing the opposite operation reverses it?
<lispy>
well...it's not really reversing it, it's changing the order of the parameters
<lispy>
for example, 1 + 2 = 3 = 2 + 1
<lispy>
so plus is symmetric with integers
<lispy>
but in matrix land, M1 * M2 != M2 * M1
<schlick>
Oh well. I've got worse things to feel dense about. :P I remember hearing people occasionally rant that people should be using strongly typed languages and they would solve all our problems (hadn't heard of a example till recently), and wondering WTF they were talking about since types seemed to be nothing more than a extreme nuisance in C, and usually a source of errors.
<schlick>
more than a extreme nuisance in C, and usually a source of errors, rather than a way of preventing them.
<lispy>
the reason you want reflexive is so that objects have unique identity under your equivalence relation
* schlick
nods about the symmetric thing. "I'm not sure I see how in math that could not work, but I'm sure there's some way I haven't thought of."
<lispy>
the whole reason for equivalence relations is because they chunk the world into disjoint sets
<lispy>
for example, things which are true and things which are false
<lispy>
those are useful disjoint sets
<schlick>
By disjoint you mean there's no overlap?
<lispy>
yup
<schlick>
Ok. At least I followed that part.
<lispy>
are you familiar with modulo?
<schlick>
The math operation?
<lispy>
7 mod 5 == ??
<schlick>
% in C (and several other things)?
<lispy>
yeah
* schlick
nods.
<lispy>
let me see if i can remeber how this example goes
<lispy>
7 mod 5 == 12 mod 5, so we say that 7 and 12 are equivalent under the equivalence relation mod 5
<lispy>
well, we need to do a bit more to show that mod 5 is an equivalence relation
<lispy>
but, it's useful because we can treat 7 and 12 as the same number in this context
<schlick>
So they might write 7 mod 5 <funny looking 3 bar equal sign here> 12 mod 5 ?
<lispy>
for example, we can determine if 5 divides 7 evenly. We check it, nope it doesn't. Now we see that 12 mod 5 is the same as 7 mod 5 and we know that 5 wont divide 12 evenly also
<lispy>
well, 7 mod 5 = 12 mod 5, but (7 == 12) mod 5
<lispy>
so 7 mod 5 IS 2 and 12 mod 5 IS 2, so those are equal
<lispy>
but if we are talking about 7 and 12 in the context of mod 5, then we can't say they are equal, but we can say they are equivalent
<lispy>
it's subtle
<lispy>
i hope that makes some sense
<schlick>
So basically it's used in the same situation you'd use equals to show something is truely "the same", but you can't because it's only the same in some ways, the way you're talking about at the moment?
<lispy>
precisely
* schlick
nods. "Makes sense."
<lispy>
yeah, you can define equivalence relations when programming and simplify some tasks
<lispy>
like checking if a thing that can take several forms is in a set
<lispy>
just define a equivalence relation so that any of the valid forms are equivalent and then check if some representative of those is in the set
<schlick>
Reminds me of how my highschool geometry/trig teacher and physics teacher taught. She was the only one that really made it click easily. I loved those classes. I suspect there's no reason I would have learned some of these symbols in them though. Just wish it was a bit easier to figure out what people were talking about. Usually when you see how they arrived at it (commonly used for geometry proofs) it's obvious.
<schlick>
about. Usually when you see how they arrived at it (commonly used for geometry proofs) it's obvious.
<lispy>
for example, we see that 2, 7 and 12 are equivalent so we'd just check if 2 is in the set
<lispy>
yeah, math instruction is tricky
<lispy>
even a good teacher can not connect with some bright students
<schlick>
Basically people forget to define what the terms mean. Leaves you basically "illiterate". You're great at playing calculator but have no idea what's going on, or why. I was there most of my school career. I did ok in class, because all you had to do most of the time was play calculator. Word problems could be tricky though, since I didn't really understand what I was doing for the longest time.
<lispy>
yeah
<lispy>
well, i think i'm going to mosey on home
<lispy>
good luck with learning about functional programming
<schlick>
Well, what the geometry/trig and physics (two classes, same instructor) did was apparently the way they usually teach it in Europe and Japan, which explains why they smoke most of us. Instead of the usual "today we'll be learning <insert formula> <writes it on the board> now play calculator with 200 problems due tomorrow" and somehow it's supposed to just magically make sense.
<schlick>
tomorrow" and somehow it's supposed to just magically make sense, she showed us how it was arrived at first, then did hands on stuff. If what you drew, or predicted, didn't work out, you knew you did it wrong, and could sort of "see it".
<lispy>
yeah, that's the math/physics instruction i had in HS (the second one)
<schlick>
Well, I basically "get" functional programming.
<schlick>
I know some Lisp, and it doesn't strike me as that hard at all.
<schlick>
But Lisp doesn't have much to do with types normally.
<schlick>
Nothing I've worked with resembles Epigram/ML/Haskell.
<lispy>
right
<lispy>
i like lisp as you may have guessed
<lispy>
but, the type system is very differente
<schlick>
Lisp makes perfect sense to me. I never have figured out why some people had so much trouble with it.
<schlick>
OO was much harder.
<schlick>
It makes great sense now. I just had a awful time figuring out what the idea was.
* lispy
waves, good luck
<schlick>
As far as I could tell in Lisp there were no types. You could put arbitrary stuff in, and if the operations could successfully occur (at runtime) it worked. Otherwise it bombed at runtime.
* schlick
waves.
<pango>
few types rather than no types (atoms, lists,...)
<schlick>
pango: I suppose that's so. The checking didn't occur before it ran. Guess that would mean it was "dynamically typed". If you messed up you didn't find out till it hit that point in your code.
<pango>
yes, whereas ML is statically typed
<schlick>
pango: So I didn't really notice types existed. They're very much 'in your face' in C and C++ (and Pascal, though that didn't seem as error prone), but as you can imagine I didn't see any benefit in them. I just remember being irritated by fowling up with numeric overflows and such.
<schlick>
It didn't seem to be "good for anything" though now I'm seeing that people were just talking about something more or less different. C seems to use types to figure out (almost only) how to produce assembly, while ML seems to use it mostly for sanity checking.
<pango>
arrays, structs, etc. are also types, you only mentionned basic types so far
<pango>
not compound ones
<pango>
(oh, and pointer types too... types that have types)
<schlick>
Well, that's true, but in the things I mentioned essentially arrays were just declaring a bunch of individual variables of the same type, which could be accessed via a index conveniently. Structs and enums seemed to be primarily ways of giving things the same name prefix. for neatness's sake.
<pango>
it's used for (some) sanity checking in C too, it just doesn't push the concept so far
<schlick>
It didn't really explain why types were supposed to be good for anything, they were just something you had to deal with in C.
<pango>
try compiling in hexa (not even asm, they have types too)
<schlick>
Quite marginal. :P It's very hard to do anything complex in C without messing up, though it may take you a long time to notice where you messed up and how. Boy are the compilers permissive. You can do stuff like void main(void) { GLorgZplartz; } and it will merrily compile it (yes I know main returning a non-integer is non-PC nowdays).
<pango>
at that point, it's easy to add integers to characters, make the products of addresses, and lots of things that make no sense
<pango>
that's why they're types, to tag binary values with some semantics
<schlick>
What's hexa?
<pango>
directly in machine code, without going thru an assembler
<schlick>
Oh, yes, programming for people that live in the matrix. ;)
<schlick>
"Do you always look at it encrypted?" "No, that's just my APL code."
<pango>
sure, but eventually all the programs you write get converted to that soup :)
<schlick>
True.
<schlick>
Typed assembly is a bit brain-injurious at this point. It seems like something that can't happen. It's a good thing of course, but it's a bit mind warping for someone that's still trying to figure out this type thing.
<pango>
in fact, types are everywhere in computing programming languages, because writing code without any types is hard
<schlick>
The simple stuff like "you can't add a string and a number" is obvious. I see how that helps, but that's not the weird stuff, like being able to say a variable can be only one of 3 things and it be checked at compile time. Something people would have killed for in C.
<pango>
well, even in assember you can write strings, ints, etc. You're still free to do lots of stupid things with them however
cmeme has quit [SendQ exceeded]
<pango>
but there's more to ocaml types than numeric types
<schlick>
The main reason typed assembly is hard to grasp is mostly because I'm still thinking of <type to declare here> <variable/array name here>. In assembly there's just memory and registers. You can't even "make" registers. So the two ideas don't seem to fit well together.
<schlick>
Again, it's a good thing, it's just hard to get used to.
<pango>
sum types are a great thing
<schlick>
I'm guessing the way you'd pull it off is specify the sort of operations you're allowed to perform on a register at the moment, or on a block of memory. That way it could check it.
cmeme has joined #ocaml
<pango>
I don't expect asm to become strongly typed, I was just saying that there's _some_ notion of types in asm
<schlick>
So far Wikipedia has helped some. Apparently the unifying idea behind types is it's a way of categorizing things mathematically. That seems pretty simple. I guess the part that leaves me a bit confused is the type inference (only somewhat interesting to me), and how type checking gets done (very interesting to me).
<schlick>
Actually there is typed assembly.
<schlick>
"Typed Assembly Language" and a slightly different take on it called TILT that's mostly concerned with relating high level languages to assembly and making sure they're equivalent.
<pango>
ok, but we're losing focus again :)
<schlick>
I suppose.
<pango>
types are a tradeoff, but a very interesting one it seems
<schlick>
The basic idea behind what I tend to look at is "how can you think about a program". I'm interested in as many ways as possible. I even find a lot of the esoteric (joke) languages interesting. It hurts your head for a while but sometimes lets you think about things in new ways. The other thing that interests me is how to prevent (not cope with after the fact) bugs.
<pango>
for the price of some loss of flexibility (some operations are not allowed anymore), you gain a lot of safety
<schlick>
So while type checking and theorem proving may not seem related, they're both able to be used to prevent bugs, so I'm interested in both.
<schlick>
Well, it looks like most of the type safe languages allow conversion between types where it's sane, they just make you /say/ it, instead of taking it upon themselves to do it, and they don't allow insane conversions. C is a bit weird. You have two choices. Have it happen automatically and be invisible (usually, but not always, safe), or specify it and give up all automatic checking...
<schlick>
always, safe), or specify it and give up all automatic checking...
<pango>
making conversions explicit can make some programs much heavier. It doesn't prevent things from being doable (that would definitely make typed languages uninteresting)
<schlick>
The whole thing reminds me of contracts with demons. You have to be very very careful how you word things, otherwise, while you may get what you asked for, you also get really undesirable things you didn't expect to be implied by what you said. :P
<schlick>
I like it explicit. It makes it easier to look at something and tell if it's wrong. If it's invisible, and your program is off doing sneaky things behind your back, it can be quite irritating.
<schlick>
It's one reason type inference leaves me a bit spooked. I'm not used to trusting the computer to "guess".
<pango>
in practice it almost always simply work
<pango>
because they're lots of hints in ocaml code already
<pango>
no operator overloading
<pango>
things that must be unique in their name space (record field names,...)
<pango>
etc.
<schlick>
It seems so. I can see the appeal. You don't have to write it on every line. I'm not sure if I'm crazy here but it seems like it'd let you do something else... You could write code that works with multiple types (by not specifying them), but is still checked against current usage. I'm not sure if that's a good thing or not. It sounds flexable, but that's not always good either.
<schlick>
It sounds flexable, but that's not always good eithe
<pango>
strongly types doesn't mean polymorphic functions don't exist
<pango>
s/strongly/strong/
<schlick>
You see what I mean, right? If you restricted a function to only working on 16 bit integers, you'd have to change that when you wanted to work with 32 bit integers. If what you're using it on can be accuratly guessed, and it can work in both situations, it just magically works, but still gets checked, with type inference.
<schlick>
I sorta like that but wonder how dangerous it is.
<schlick>
Mostly in that what doesn't get checked if you don't specify it.
<pango>
mmmh to work on different "number sizes" you'll require either templates or functors
<pango>
I find it disturbing that you're always using numeric types in your examples
<schlick>
Well, I /think/ it would just work, with type inference, so long as the constants inside were smaller than or equal to the smallest number size you wanted to work with. It should be able to figure out which size numbers you're passing to it and therefore how big the variables inside should be.
<schlick>
Why's that? :)
<schlick>
Really numeric types are the most dangerous.
<pango>
because numeric types are something like 5% of the types I use, and I don't find them exciting at all ;)
<schlick>
Numeric underflow and overflow and pointer arithmetic are probably the most common mistakes in C, at least after you get past the stuff you can fairly easily learn to avoid (e.g. the dangers of C's switch-case statement's automatic fall-through).
<pango>
of course, some applications make heavy use of them
<schlick>
Strings are sort of dangerous but that's still pointer arithmetic (on array indexes).
<pango>
ocaml doesn't allow pointer arithmetics (in fact you only have references, not plain pointers)
<schlick>
Yes, but it's interesting from the point of "holy crap, that doesn't happen here". :P
<pango>
on the other hand it doesn't catch numeric overflows/underflows
<schlick>
Yes, that's one sad thing about it.
<schlick>
Apparently there's a exception you can catch. I'm told Standard ML and Haskell don't have the numeric underflow/overflow problem.
<schlick>
I don't like exceptions much but apparently I'm strange for that.
<pango>
it doesn't seem too difficult to write a module that overloads standard operators with hardened versions, but it seems the cost is a bit high
<schlick>
They end up getting abused like goto (because they /are/ goto), and really, what /is/ a exception? Either you handle something or you don't. I don't see how you can have a "handled exception". If it's handled, it's not a exception... Seems like a excuse to arbitrarily rearrange the code.
<pango>
exceptions remove a range of bugs, but add their own new bugs
<pango>
I think gain > loss however
<schlick>
Well, from C being a lot like juggling chainsaws, while drunk, and being hit over the head by angry monkeys, you learn some tricks to cope. One is /ALWAYS/ read the return value of any function that might even theoretically fail, then handle it ASAP. If you do that you don't seem to need elaborate exception handling schemes. They seem to sort of aggrivate a problem.
<schlick>
Then again, I grew up with goto, so maybe I just have gotophobia. :P I've never missed it.
<pango>
exceptions are suppposed to be better there by moving special cases out of the common path
<pango>
making code more readable
<schlick>
Well, I'm not sure that's good though.
<pango>
and also, people are notorious at *not* checking return values
<pango>
return values are also a problem with strong typing, because they must be consistent with expected types
<pango>
and magic values suck
<schlick>
For instance, they know if you set or declare a variable very far from where it's used, there's likely to be bugs in its usage (see Code Complete). It seems like handling errors would be subject to the same problem. The other thing is I'm not sure there's such a thing as "generic" error handling. What you need to do when something goes wrong is usually specific to what you're doing at the time.
<schlick>
when something goes wrong is usually specific to what you're doing at the time.
<schlick>
Yes, people /are/ notorious for not checking return values. If you spend long with C you'll start though. :P
<pango>
as I said, using exceptions prevents some kinds of bugs, but add new kinds
<schlick>
And magic values may suck. I don't deny that. I'm just not too sure what's better. People tell me to look at Common Lisp to see good error reporting.
<pango>
(error conditions hidden by too coarse exception handlers...)
<pango>
(error conditions misinterpreted by exception handler because the same exception can be raised from several places)
<pango>
probably more
<schlick>
It's worth noting that people had a lot of the same problem with goto. Basically arbitrarily lopping off parts of code from the execution path by sticking it somewhere else, or skipping something, tends to be really bad.
z|away_ is now known as z|away
cmeme has quit ["Client terminated by server"]
<schlick>
If it's in neat little blocks, and you need to insert a check, you can stick it one place and know everything will hit it.
z|away has left #ocaml []
<schlick>
Since it can't skip past it. And it's nice and close to the thing you need to check, so it's easy to tell what's going on.
cmeme has joined #ocaml
pango_ has joined #ocaml
<pango_>
of course, they're ways to avoid that. Mainly, be cautionous about exceptions handling
<schlick>
By the way I'd be interested in your opinions on how to handle errors better.
<schlick>
Than magic numbers that is.
cmeme has quit [Client Quit]
<pango_>
well, static typing removes whole classes of runtimes errors, that's a start
<schlick>
Yes, you can use goto and be cautious too. I just tend to prefer to avoid it. I'm one of those odd people that doesn't mind losing powerful constructs if I really don't need them, and removing them prevents some errors. Seems to save some code too. On a goto-only implementaiton of BASIC (really old ones...) you got all the "fun" of implementing your own loop structures and call/return structures.
cmeme has joined #ocaml
<pango_>
what's left is all what couldn't (or cannot) be checked statically
<schlick>
the "fun" of implementing your own loop structures and call/return structures.
<schlick>
Agreed. Personally I love the idea of taking out every error that can be prevented at compile time. I'm a little obcessed with that.
<schlick>
There are some things you can't though.
<schlick>
For instance, if your program needs to work with the network.
<schlick>
You can't keep the other end from going down.
<pango_>
or any I/O for that matter
<schlick>
Well, some I/O is pretty dependable. I'm not much worried about my keyboard suddenly stopping. It's possible but not likely. However some things are a lot less sure, like the network thing.
cmeme has quit [Client Quit]
<pango_>
in pure functional programming, I think error checking can be done with monads (since exceptions have imperative traits, they're not available)
cmeme has joined #ocaml
<pango_>
can't tell how it compares in readability, etc.
<pango_>
s/checking/handling/
cmeme has quit [Client Quit]
<schlick>
Not real clear on the monad thing either. Lisp is impure. It has loops. You usually learn about recursion (it hurt my head a little at first but I picked up on it in a hour or so, the recursive maze solving algorithm example helps explain why you'd use it), but you don't have to do it. The idea in pure functional programming seems ok to me, but I don't see how to handle I/O without breaking it.
<schlick>
seems ok to me, but I don't see how to handle I/O without breaking it.
<schlick>
I do know monads are the way they do it.
<schlick>
I just haven't looked into it much.
<schlick>
monads are widely considered very confusing.
cmeme has joined #ocaml
<schlick>
Whether this is a readability issue, or just because people usually have a lot of trouble understanding functional programming I don't know.
<lispy>
schlick: youwouldn't say that lisp isn't typed because you can ask it what the type of something is
cmeme has quit [Client Quit]
<lispy>
contrasted with assembly where you have no types essentially :)
<schlick>
Personally functional programming made decent sense to me in next to no time. Again, C punishes side effects extremely harshly (you write foo(bar(),baz()); what do you think will happen first? whatever you think is likely wrong, because bar or baz could be executed in any order), so getting rid of them seems like a capitol idea.
cmeme has joined #ocaml
<lispy>
would'nt bar happen first, then baz then foo?
<schlick>
lispy: no.
<lispy>
baz then bar?
<schlick>
It's not standardized. And quite often, in practice, it depends on the setting of your optimizer. The optimizer is free to reorder functions as arguments to functions. If any of those functions did I/O you will get VERY mysterious behavior.
<lispy>
oh right
<lispy>
wow, that's lame
<lispy>
even in C99?
cmeme has quit [Client Quit]
<schlick>
The workaround is to /force/ the order, by doing bleh=bar(); foo(bleh, baz());
<pango_>
I don't think it's lame
cmeme has joined #ocaml
<schlick>
So far they're satisfied with not having C be a dataflow language, so it does at least execute separate statements in the order the programmer specifies. ;)
cmeme has quit [Client Quit]
<schlick>
lispy: and yes, even in C99.
<schlick>
It's been that way forever, I doubt they'll change it. After all, they didn't remove gets() after the morris worm.
cmeme has joined #ocaml
<schlick>
There's probably some old PDP/11 code out there that uses the function order execution to determine what level of optimization it's being compiled with which it uses to determine something else (the user interface or god knows what). Hey, it's a FEATURE! :P
cmeme has quit [Read error: 104 (Connection reset by peer)]
pango has quit [Read error: 110 (Connection timed out)]
cmeme has joined #ocaml
cmeme has quit [Client Quit]
cmeme has joined #ocaml
cmeme has quit [Client Quit]
cmeme has joined #ocaml
cmeme has quit [Client Quit]
cmeme has joined #ocaml
cmeme has quit [Client Quit]
cmeme has joined #ocaml
cmeme has quit [Client Quit]
bzzbzz_ has quit [Client Quit]
m3ga has joined #ocaml
bzzbzz has joined #ocaml
cmeme has joined #ocaml
cmeme has quit [Client Quit]
cmeme has joined #ocaml
cmeme has quit [Client Quit]
cmeme has joined #ocaml
cmeme has quit [Client Quit]
cmeme has joined #ocaml
cmeme has quit [Client Quit]
cmeme has joined #ocaml
cmeme has quit [Read error: 104 (Connection reset by peer)]
<lispy>
wow, that's annoying
cmeme has joined #ocaml
cmeme has quit [Client Quit]
cmeme has joined #ocaml
cmeme has quit [Connection reset by peer]
cmeme has joined #ocaml
cmeme has quit [Read error: 104 (Connection reset by peer)]
cmeme has joined #ocaml
cmeme has quit [Client Quit]
cmeme has joined #ocaml
cmeme has quit [Client Quit]
cmeme has joined #ocaml
cmeme has quit [Read error: 104 (Connection reset by peer)]
cmeme has joined #ocaml
cmeme has quit [Read error: 104 (Connection reset by peer)]
cmeme has joined #ocaml
cmeme has quit [Client Quit]
Revision17 has quit [Read error: 110 (Connection timed out)]
cmeme has joined #ocaml
cmeme has quit [Client Quit]
Revision17 has joined #ocaml
cmeme has joined #ocaml
cmeme has quit [Client Quit]
cmeme has joined #ocaml
Smerdy is now known as Smerdyakov
cmeme has quit [Remote closed the connection]
cmeme has joined #ocaml
NivegnaEnigma has quit ["Lost terminal"]
Smerdyakov has quit ["Leaving"]
Nivegna has joined #ocaml
munga has joined #ocaml
m3ga has quit ["disappearing into the sunset"]
munga has quit ["Client exiting"]
<flux__>
schlick, haskell has two kinds of integers, those that do overflow (without warning) and those that don't (because they are limited by available memory)
shirogane has quit [Remote closed the connection]
_JusSx_ has joined #ocaml
Oejet has joined #ocaml
rillig has joined #ocaml
revision17_ has joined #ocaml
Revision17 has quit [Read error: 110 (Connection timed out)]
Nivegna has quit [Remote closed the connection]
Submarine has joined #ocaml
ski has quit [Read error: 110 (Connection timed out)]
Submarine has quit [Remote closed the connection]
Submarine has joined #ocaml
Skal has joined #ocaml
m3ga has joined #ocaml
m3ga has quit ["disappearing into the sunset"]
rillig has quit ["exit(EXIT_SUCCESS)"]
malc_ has joined #ocaml
smimou has joined #ocaml
mellum_ is now known as mellum
vodka-goo has joined #ocaml
bzzbzz has quit ["leaving"]
Raziel has quit ["Yo soy goma. Tú eres cola."]
Raziel has joined #ocaml
Submarine_ has joined #ocaml
Submarine has quit [Nick collision from services.]
Submarine_ is now known as Submarine
vincent has joined #ocaml
vincent has left #ocaml []
pnou_ has quit [Read error: 104 (Connection reset by peer)]
Maledict has joined #ocaml
<Maledict>
hi
<Maledict>
please, a question
<Maledict>
I defined the data type
<Schmurtz>
you wan't a question ?
<Schmurtz>
;)
<Maledict>
type eval =
<Maledict>
| Int of int
<Maledict>
| Bool of bool
<Maledict>
| String of char list
<Maledict>
| Char of char
<Maledict>
etc.
<Maledict>
let esseuno=[Char('a');Char('b')];;
<Maledict>
val esseuno : eval list = [Char 'a'; Char 'b']
<Schmurtz>
("String of string" may be better than "String of char list")
<Maledict>
this happens when I build esseuno
<Maledict>
I want esseuno of eval type, not eval list
<Maledict>
String of string may solve, but I must do String of char list
<Schmurtz>
ok
<Schmurtz>
for me, "val esseuno : eval list = [Char 'a'; Char 'b']" is not a ocaml statement
<Maledict>
no, that's the answer of interpreter
<Schmurtz>
so, I can't understand your problem
<Schmurtz>
ok ;)
<Maledict>
I need esseuno of eval type
<Schmurtz>
let esseuon = String(['a','b']);;
<_JusSx_>
Maledict: italiano?
<Schmurtz>
['a': 'b'] is of type char list
<Schmurtz>
so String(['a';'b']) is of type eval
<Maledict>
si, italiano
<Maledict>
ok, thanks Schmurtz, I try
<Schmurtz>
if you write [Char('a');Char('b')], you create a list containing eval elements)
Maddas_ has joined #ocaml
<Maledict>
let esseuon= String(['a';'b']);;
<Maledict>
ok, thank you very much Schmurtz, I solved
<Schmurtz>
you're welcome
batdog|gone is now known as batdog
batdog is now known as batdog|gone
<Maddas_>
Hi! Are MetaOCaml questions on-topic here?
<Schmurtz>
if somebody can answer you, yes ;)
<Maddas_>
Why is .< 1 ; 2 >. a syntax error? :-)
* Schmurtz
has never used metaocaml
<Maddas_>
(FTR, something like .< ( 1 ; 2 ) >. isn't, but I don't think that's a feature)
Maddas_ is now known as Maddas
Smerdyakov has joined #ocaml
<Maddas>
Hello, Smerdyakov :-)
<Smerdyakov>
Maddas, hello. Why do I get a special smiling greeting today?
<Maddas>
Heh. Just because I haven't seen you for a long time.
<kmag>
Smerdyakov: he's still drunk
<Smerdyakov>
I've been in her 24 hours a day for a while. I guess you haven't?
<Smerdyakov>
s/her/here
<Smerdyakov>
(Perhaps bad typo!)
<Maddas>
No, I haven't been here for a long time.
<Submarine>
Smerdyakov, You PERVERT.
<schlick>
Smerdyakov: Going to order those books as soon as my credit card company gets my check for last month (should be today or Monday). Does the book on types you showed me explain how type checking occurs?
<Smerdyakov>
schlick, yes. There are exercises to write type checkers and interpreters for many languages, if I remember correctly.
<Smerdyakov>
schlick, why don't you pay your CC bills electronically?
<schlick>
Smerdyakov: Cool! :) BTW, thanks for pointing me at Epigram.
<schlick>
Smerdyakov: I suppose I could. I have to go through some contortions to get my bank to allow that, that I haven't done. There are other bills I have to pay with check or money order (and they much prefer money order), so I just use money orders for everything.
<Smerdyakov>
I'm down to only needing to pay my rent by check.
<Smerdyakov>
Everything else is automatic by e-lectronic methods.
<schlick>
I have a lot of things I pay for by money order, but most of them aren't monthly. Just my rent. Various insurances I still pay for that way. The phone bill is rolled into the credit card bill. It made for less headaches that way.
<kmag>
When were these books suggested?
<Smerdyakov>
The year 1849.
* kmag
is looking for some good language/compiler books.
<Smerdyakov>
schlick wants to learn about formal methods for programming correctness.
<Smerdyakov>
I recommended reading "Types and Programming Languages" by Benjamin Pierce and then "Coq'Art" by Bertot & Casteran.
<Smerdyakov>
...because I think that dependent type systems are going to prove themselves to be the best tools of the kidn schlick asked about.
<schlick>
I've weeded out some decent compiler books, if you're interested kmag.
<kmag>
I have the dragon book, that's it
<schlick>
And from reading a paper called "A Type System Equivalent to a Model Checker" I'm convinced types will be at least as good as a theorem prover for most purposes, just may need a model checker still for counterexamples.
<schlick>
kmag: So do I, unfortunatly it's so far out of date it doesn't include explanations of things you'll read about now.
<Smerdyakov>
I didn't find that work very enlightening. The connection seemed pretty forced.
<Smerdyakov>
And we've already talked about why counterexamples are not computable for interesting systems. :)
<schlick>
kmag: Engineering a Compiler by Keith Cooper, Advanced Compiler Design and Implementation by Steven Muchnick, and Optimizing Compilers for Modern Architectures by Ken Kennedy
<kmag>
schlick: thanks :-D
<schlick>
kmag: I have a feeling none of those will be very "introductory" but it seems nothing is along these lines. I just hope enough insanity gets me through.
<kmag>
schlick: in that order?
<Smerdyakov>
schlick, what happened to Appel's books?
<kmag>
I'm mostly interested in JITs
<Smerdyakov>
kmag, in what context?
<schlick>
kmag: I arrived at those books mostly by making sure they covered the topics I was having trouble getting information on (e.g. writing backends that can do optimizations on SSA form), and looking at reviews. I don't know as any particular order is involved. The first is mostly on the math behind it. The second is almost entirely implementation. The third seems to be optimization specific.
<schlick>
almost entirely implementation. The third seems to be optimization specific.
<schlick>
Smerdyakov: If I can survive the books I mentioned, would I need the Appel compilers in ML book?
<Smerdyakov>
schlick, probably.
<schlick>
Smerdyakov: Or are you thinking it'd help in the task of surviving with minimum limbs lost?
<schlick>
Ok, let me dig on Amazon.com a little.
<Smerdyakov>
schlick, Muchnick assumes you know the basics, and it also has the worst form of algorithm presentation ever.
<schlick>
Smerdyakov: I figured it wasn't very friendly from what most people had said. The only one I own right now is the dragon book, which isn't that friendly or that hard (kinda disorganized though), but doesn't cover /lots/ of modern stuff.
<Submarine>
Dragon is totally outdated.
<schlick>
Smerdyakov: "Modern Compiler Implementation in ML" ?
<Smerdyakov>
I haven't gotten the impression that you're interested in advanced optimization topics, so I predict that Appel is all you will want to read.
<Smerdyakov>
That's the one.
<schlick>
Ok.
<Smerdyakov>
Don't you have a university library around where you could check these books out?
<Submarine>
advanced optimization, for many authors, seems to be "how to compile FORTRAN for fast computations"
<Submarine>
Smerdyakov, c'mon.. students entering the library? no way
<Smerdyakov>
Submarine, he's not a student.
<schlick>
Smerdyakov: I'm far more interested in correctness first, maintainability second, and efficiency last. But I can't afford to ignore it. Main reason for interest in it at this point is once I start writing my "real" compiler I want to have the back end well suited to optimization, so I don't have to go back and re-engineer it.
<Smerdyakov>
(In the institutional sense)
<Submarine>
I've made an assignment for students to write a compiler from math expressions to JVM.
<Submarine>
I wonder how many will see the strong hints that I gave that they should implement a postfix tree traversal.
<Smerdyakov>
Submarine, with a library for emitting JVM bytecodes?
<Submarine>
yes, ASM
<schlick>
Submarine: Apparently I have the world's strangest hobby. :/
Maddas has left #ocaml []
<Submarine>
compiling to real archs is more painful
<Smerdyakov>
Submarine, "arches"
<kmag>
Submarine: where do you teach?
<Submarine>
ec. polytechnique near paris
Skal has quit [Remote closed the connection]
<schlick>
Random, possibly dumb question. What is the connection between ML and France? If this seems dumb I haven't read the history of ML, other than knowing the creator worked on theorem provers.
<Schmurtz>
ocaml is written by french researchers
<Schmurtz>
that the only one connection between ML and france
<schlick>
I'd forgotten about that.
<Submarine>
and caml is used in some of the french higher education system for introduction to programming
<kmag>
Submarine: why not have students target the Ocaml VM ?
<Submarine>
kmag, because these students don't know caml
<kmag>
(instead of the JVM, in the programming exercise you mentioned)
<Submarine>
and also because caml has no JIT
<schlick>
The reason I asked is it seemed a little unusual. One of the first days I was here someone mentioned several French people being nice. And then a French teacher showed up. So I thought I'd ask.
<Schmurtz>
Submarine, there's one JIT compiler for ocaml
<kmag>
Submarine: I'm not familiar with the actualy ZINC bytecodes... Are they very Ocaml-specific?
<Submarine>
the interest being to demonstrate how they can speed up some computations by dynamically compiling expressions... then it ends up in native code
<Submarine>
kmag, Ocaml has its own special model of bytecode.
<Submarine>
my students don't know ocaml
bewo has joined #ocaml
<kmag>
about all I know about the ZINC bytecode is that it's stack-based
<Oejet>
Submarine: What languages does your students know?
<Schmurtz>
Submarine, what's your real name ? I perhaps know you : U was a student at the ec. polytechnique last year ;)
<Submarine>
Java
<Submarine>
Schmurtz, David Monniaux; who are you?
<kmag>
and about all I know about ocamlopt is that it uses untyped lambda calculus as one of its intermediate reps
<Schmurtz>
I'm Damien Bobillot, but I don't think you've seen me
<Submarine>
if you did the majeure 1, I was the guy giving the caml course
<Schmurtz>
ok
Skal has joined #ocaml
<malc_>
Submarine: was it you who had a page with proofs on ocaml's set/map implementations?
<Smerdyakov>
I just assume that they're sound in my proofs. ;)
<Submarine>
i have such implementations, so do other people
<Submarine>
i should put it online
<Smerdyakov>
Submarine, on the implementation, or on a Coq version of it?
<Submarine>
I could give both
<mellum>
Does anybody know where "caml_apply2" which appears in compiled binaries comes from?
<Smerdyakov>
How do you connect the ML version with a machine-checkable proof?
<Submarine>
using the coq export system
* malc_
vaguely recalls a page with proofs, and discovery of a bug in set(map?)s rebalacing(?)
<Submarine>
it's JC Filliatre
<malc_>
oh yeah
<malc_>
those french names sound all the same to me
<malc_>
weird and unpronouncable
<mellum>
french pronounciation isn't particularly difficult
<Submarine>
my implementation has map2 stuff
<Submarine>
i.e. you combine two maps
<Submarine>
and it also has optimizations using ==
<malc_>
Submarine: heh, just found that we conversed briefly in 2002.. on the subject of functor specialization
<Submarine>
who are you?
<malc_>
that's the question you also asked back then
<malc_>
no one in particular, innocent bystander if you wish
Oejet has quit [Remote closed the connection]
<pango_>
mellum: all caml_applyn are generated from a macro somewhere
<mellum>
pango_: Are they then put in some .a file?
<mellum>
Or always freshly generayed?
<pango_>
I saw it in apply_function in asmcomp/cmmgen.ml
<pango_>
when I was looking for them (from reading a profiling dump)
<mellum>
They are not in the .s if I compile with -S...
<pango_>
I suppose they're always inlined, something like that
<mellum>
inlined? No, they are single functions when disassembling
<mellum>
Ah, yes. they get emitted to some temporary file
<schlick>
Does anyone know if the more recent editions of Appel's books are better than the older ones? There's some frighteningly bad reviews on Amazon.com (2 and 3 stars, out of 5).
<Smerdyakov>
schlick, do you have a link to the reviews?
<schlick>
He has a large line of books (at least C, Java, and ML), if you look at the first edition (i.e. hardback) of the ML book, or any of the Java books, you'll see. Most of the complaints break down to not explaining what's being done, or why.
<schlick>
I'll dig up the ML one, hang on a sec.
<schlick>
The new version doesn't have a rating yet.
<Smerdyakov>
I don't want to find the pages. Can you give me a link?
<Smerdyakov>
I have a feeling that the negative reviews are coming from less serious students or from people who have to teach them.
bewo has quit ["Leaving"]
<schlick>
I just thought I'd ask. It is worth noting that there's a new edition of the ML book, and, I think, the C book, but there aren't any ratings for them yet. I know it's a hard topic. Just when I saw the whole line getting bad reviews it spooked me a bit.
<schlick>
I did think the one "learn a real language" comment was amusing. :P I admit all this strong typed stuff is hard to wrap my head around just now, but even at this point it's easy to see why it's better than C or Java.
Skal has quit [Read error: 104 (Connection reset by peer)]
Skal has joined #ocaml
<schlick>
Smerdyakov: What do you think of http://www.amazon.com/gp/product/3540654100 The main reason I'm looking at it is it's come up when I've looked up some terms (namely abstract interpretation).
<Smerdyakov>
I've never used it.
ski has joined #ocaml
<schlick>
Does it look like it'd be worth getting? It seems to be the only general "how to statically analyze programs in general" book. Thought it might help me know what people ment when they were talking about using abstract interpretation to minimize the states to check for model checking and such.
<Smerdyakov>
Probably
<schlick>
You think it would then?
<Smerdyakov>
Yes.
<schlick>
Ok. Thanks. :)
ski has quit [Read error: 104 (Connection reset by peer)]
rq has quit [Nick collision from services.]
mercurylala has joined #ocaml
ski has joined #ocaml
<quamaretto>
Jens Palsberg... Had the guy as an administrator for the CS 101 Java course thing at Purdue.
<Smerdyakov>
quamaretto, oh, and I bet you think that makes you SO special!
<quamaretto>
Nah, I actually dislike Purdue
<quamaretto>
If I had to go back to school it would be somewhere else.
rillig has joined #ocaml
<quamaretto>
The Purdue CS department thinks, I suppose, that presenting basic material in the most difficult way possible is effectively the same as presenting difficult material.
<rillig>
quamaretto: You department concentrates on research, rather than teching? :)
<rillig>
s/tech/teach/
enthalpyX has joined #ocaml
dylan has joined #ocaml
<dylan>
There wouldn't happen to be anything like erlang's mnesia for ocaml, would there?
<Smerdyakov>
What is it?
<dylan>
It's a distributed relational database that uses erlang's native data structures.
<Smerdyakov>
I'm not aware of such a thing.
<dylan>
Essentially, if you want mutable state in erlang, you use mnesia.
<dylan>
Darn.
<dylan>
It'd be very cool to have it in ocaml, for the type safety.
<quamaretto>
I need to learn me some erlang one of these days.
<dylan>
it's slick. Or sick. Being able to change the workings of a running server without stopping it or disconnecting the clients is quite useful.
<dylan>
and as far I know, it doesn't have mutable variables.
<kmag>
dylan: I've only dabbled with Erlang, but it seemed to me that its record types only offered access by position
<dylan>
it has named records.
<dylan>
Ugly syntax, but it has them.
<kmag>
dylan: so they aren't used much
<kmag>
dylan: or they aren't used much in tutorials?
<dylan>
they're used all the time with mnesia
<kmag>
but how easy is it to send them as messages between processes?
<kmag>
is it cumbersome?
<Schmurtz>
there is a marshalling system
<Schmurtz>
and a easy to use socket system
* Schmurtz
look at the doc
<Schmurtz>
+s
<kmag>
it seems to me that messages between processes almost always use position in the message to access fields of the message
<dylan>
kmag: you can send any data between processes. You can even send functions, provided it's on the same machine (I think)
<kmag>
(I don't think 'field' is the proper term)
<Schmurtz>
dylan, even functions ?
<dylan>
function references, I seem to remember from a tutorial, can be sent to another erlang process. Because erlang processes are in the same memory space.
<dylan>
if the erlang process is on another machine, then, it won't work.
malc_ has quit [Remote closed the connection]
<Schmurtz>
ok
<dylan>
It's transparent to send to another machine, of course. :)