<ec>
micahjohnston: wait, so if you're into drugs and booze now, are you into porn, too?
<ec>
wait, I can't remember if you've gotten laid
<ec>
man, nobody's awake
<ec>
stupid Alaska timezone
alexgordon has joined #elliottcable
alexgordon has quit [Client Quit]
<ec>
alexgordon popped in … poopedi n
<joelteon>
i am this awake
<whitequark>
ec: i am
<whitequark>
awake
<joelteon>
whitequark doesn't realize i exist
_whitelogger has joined #elliottcable
_whitelogger has joined #elliottcable
<ec>
hi whitequark
<whitequark>
hi
<purr>
whitequark: hi!
<whitequark>
purr: hi
<purr>
whitequark: hi!
<whitequark>
purr: hi
<purr>
whitequark: hi!
<whitequark>
purr: hu
<whitequark>
guess if whitequark slept tonight, the game
<whitequark>
in the box office right after "LLVM, The Movie"
<whitequark>
I'd watch it.
<whitequark>
it would probably be the most boring movie ever made, and the longest one, but I'd still sure as fuck watch it.
<whitequark>
ocaml is absolutely amazing.
<whitequark>
it's functional, on one hand, and on the other one doesn't have that obnoxious academicity which such languages often have
<whitequark>
- lack of libraries
<whitequark>
- oversimplified syntax
<whitequark>
- dumb incompatibilities with common conventions
<whitequark>
- implementation worse than Ruby MRI
<whitequark>
etc
<whitequark>
IT EVEN WORKS ON WINDOWS
<prophile>
something something ghc
<whitequark>
something something monads
<whitequark>
>common conventions
<whitequark>
imperative IO is the commonest convention of all common conventions.
<prophile>
monads aren't incompatible with common conventions
<prophile>
in fact as far as the IO monad goes, it's the opposite
* whitequark
sighs
<prophile>
it allows the common convention in what's still a purely functional language
<whitequark>
see, *I* don't care, really, I could write the compiler in Haskell, or even in SML
<whitequark>
go out, pick J. Random Hacker, record the time it takes him to be accustomed with monadic IO and general pureness
<whitequark>
(actually I do and I dislike haskell for a variety of reasons I'm *not* going to enumerate, lest a flamewar will erupt)
<prophile>
I'm intrigued
<whitequark>
(which would be irrelevant, whereas J.R.H bit *is*)
<prophile>
well, I'm not sure on the JRH bit
<whitequark>
I'll explain:
<prophile>
I didn't find it too much to adjust to
<prophile>
but that's anecdotal at best
<whitequark>
I'm writing a language for someone who's essentially a JRH.
<whitequark>
this is an explicit design goal.
<prophile>
then purity probably isn't a good route
<whitequark>
so, I'm sort of viewing languages via this lens, at this very moment at least.
* whitequark
nods
<whitequark>
exactly my point
<whitequark>
don't expect me to be able to discuss languages in several completely distinct contexts simultaneously.
<prophile>
for the sake of full disclosure then
<prophile>
for my current final-year university project
<prophile>
i'm knee-deep in semantics and formal modelling
<prophile>
so i'm looking at things through that lens
<whitequark>
it takes me literally days to adjust my brain to perform the Foundry design process, so it affects my view immensely
<prophile>
I remember being taught paws
<whitequark>
well.
<whitequark>
on the JRH scale, OCaml is unusually high for a functional language.
<whitequark>
it's hacky, it's imperative, it's dirty, and it feels amazing
<whitequark>
... that last part might or might not have been said about a language
<whitequark>
regardless.
<whitequark>
I hope I have conveyed my point.
<whitequark>
oh.
<whitequark>
prophile: say, do you think mutable data structures can ever be non-invariant?
<prophile>
what do you mean by invariant?
<whitequark>
well
<whitequark>
there are covariant collections... think Array<Base> x = Array<Derived>()
<whitequark>
and they are unsound
<prophile>
right
<whitequark>
in presence of mutability.
<whitequark>
so it seems to me that the only sane idea is to permit variance through immutable "views"
<prophile>
I'm... actually not following here
<whitequark>
well
<prophile>
probably terminology I don't know
<whitequark>
let's say:
<prophile>
oh, I see
<prophile>
so x is fine if it's only being read
<whitequark>
\o/
<whitequark>
exactly
<prophile>
immutable views are fairly sensible
<prophile>
although you could go for a copy
<prophile>
(which wouldn't necessarily be that terrible if you have sensible copy-on-write semantics or such)
<whitequark>
why I'd need to copy? even if the aliased original is mutated, the program is still valid
<prophile>
true, but then your view at the "higher class level", shall we say, is immutable
<prophile>
which means you have to consider both immutable and mutable arrays
<whitequark>
oh, you mean that the immutability guarantee is stronger
<prophile>
that's an extra "moving part", although that might be fine if you want to handle immutable arrays anyway
<prophile>
no, just that rather than having one "data type", the mutable array
<prophile>
you now have two
<prophile>
arrays, immutable and mutable
<whitequark>
well, it's not very big problem, since (
<whitequark>
I'm simplifying) I also have immutable and mutable array typeclasses
<prophile>
in that case that's fine
<prophile>
if you didn't, it would be introducing extra complexity
<whitequark>
there's sort of another problem though
* whitequark
scratches his head
<whitequark>
currently, Foundry's type system (a variant of HM) is not strong enough to represent this constraint
<whitequark>
that is... "if this view is immutable, make its parameter covariant"
<prophile>
again, the terminology has whistled past me
<prophile>
I'm on familiar with covariance in this context referring to functors?
<prophile>
s/on/only/
<whitequark>
it's the same term, from category theory
<whitequark>
but in this case it's applied to collections
<prophile>
so what's a view's context?
<prophile>
uh
<prophile>
that made no sense
<prophile>
disregard
<prophile>
ahem
<prophile>
so what's a view's parameter?
<whitequark>
type 'a array
<whitequark>
or rather
<whitequark>
type 'a immutable_array and 'a mutable_array
<whitequark>
they're both views
<whitequark>
and they're parametric types
<whitequark>
so, this definition I just wrote down is invariant
* whitequark
sighs
<whitequark>
you're not familiar with ocaml are you?
<whitequark>
then it'll be lost on you.
<prophile>
unfortunately not
<whitequark>
ok, let me try again
<prophile>
I probably just need to think about this for a bit
<whitequark>
you certainly know what a parametric type is
<whitequark>
so. let's say we have type 'a list, and this list is the usual functional list--immutable all the way down
<prophile>
gotcha
<ec>
woah people
<whitequark>
you know
<whitequark>
you're fast :D
<whitequark>
that's good.
<ec>
lolwat hi
<purr>
lolwat
<whitequark>
ec: hi
<prophile>
hullo elliott
<whitequark>
prophile: ok. so. I take it you understand my problem then?
<ec>
whitequark: you're making me want to ocaml
<prophile>
whitequark: still processing this
<prophile>
give me a minute
<whitequark>
the transition from 'a mutable_array to 'a immutable_array cannot be typechecked by the foundry type system
<whitequark>
I *can* guarantee this within library code, but the fact that this is essentially a hack around the type system which can make the program become memory-unsafe makes me very uneasy.
<whitequark>
prophile: I think something like this may work:
<whitequark>
if a reference, be it a field inside a record or an element inside an array, is marked as covariant
<whitequark>
forbid mutating it.
<whitequark>
so I'll turn it the other way around: the array won't be covariant because it's immutable
<whitequark>
but rather immutable as a side effect of being covariant
<whitequark>
which is *completely* unintuitive, but type-safe and is likely of no concern to almost all users.
<prophile>
that actually sounds quite reasonable
<whitequark>
\o/
<whitequark>
also
<whitequark>
I want to bounce the main idea of foundry off you
<prophile>
shoot
<whitequark>
instead of making the type system stronger, say with dependent types and such, I left the TS at roughly HM level, and instead taught the compiler to make code weaker
<whitequark>
specifically: when the typechecker/inferencer cannot type some piece of code, it partially evaluates it according to a well-defined set of rules, and then tries again
<whitequark>
even more specifically: in addition to HM type variables, henceforth "poly" type variables ('a, 'b, ...), I've introduced "mono" type variables, henceforth '_a, '_b, ...
<whitequark>
both of them, as usual, convey the notion of type equivalence, but instead of let-polymorphism, "mono" type variables drive what I call let-specialization
<whitequark>
that is, when the compiler looks at an application, and the type of operands/result is more specific than the type of the applied function, *and* the applied function is known to be constant
<whitequark>
it duplicates the applied function body, and replaces the callee in application with this duplicated body, and substitutes the "mono" type variables inside the function body to make it more specific.
<whitequark>
then, it folds constants. then, it performs let-specialization. repeat until the process converges.
<prophile>
can you be certain it always _does_ converge?
<whitequark>
if you memoize specialized functions, this process can successfully assign types to polymorphic recursive and mutually recursive functions, so I'd say that yes, it always terminates.
<whitequark>
I think you can sketch the proof based on the fact that it the process does not introduce newly abstract types
<prophile>
fair enough
<whitequark>
so at worst, it'll create (all functions × all tuples of all possible types)
<whitequark>
you get the idea
<prophile>
okay, if you'll forgive my engaging layman mode
<prophile>
was going to say something along those lines actually
<prophile>
that's potentially a lot of copies
<whitequark>
oh, yes, but you asked me if it converges in a finite number of steps :D
<whitequark>
now I go into language-lawyer mode and say this:
<whitequark>
on non-pathological input, all the algorithms I employ scale nearly linearly with size
<whitequark>
the specialization thingy is based on Ole Agesen's Cartesian Product Algorithm, and I think he found that it's nearly linear in real-world Self code
<prophile>
fair enough then
<whitequark>
oh I forgot the most important thing: this allows a language with static, HM-derived type system to "feel" like a dynamic language, Ruby or something
<whitequark>
so, what do you think?
<whitequark>
there's also the fact that you can first launch the whole contraption in "dynamically typed" mode in order to do even less restricted metaprogramming, and not care at all in which phase ("run" or "compile") your code is being evaluated
<joelteon>
i used to think it wouldn't be annoying to be ignored
<joelteon>
but now the conversation moves places without me
<prophile>
terrifying places
<joelteon>
yeah
<whitequark>
I'm now reading one of the papers on ML
<whitequark>
(value restriction)
<whitequark>
it's one of those times you cannot really decide if something is a feature [of a type system], or a loophole which was so cleverly abused it seems like a feature
<whitequark>
and I'm referring to the fact that functions which never return, have type (anything -> 'a)
<joelteon>
haha, like the entirety of perl
<whitequark>
and that e.g. empty list has type ('a list)
<joelteon>
I tried to solve luhnybox in perl
<whitequark>
so this corresponds very nicely to the return type of List.hd [], which never returns
<prophile>
the latter case seems to make sense
<whitequark>
and also unifies very nicely with anything else, which is safe
<prophile>
the former, mrfhlh
<joelteon>
prophile: ask whitequark if that means that List.hd [] actually hangs indefinitely
<joelteon>
or what happens
<joelteon>
please
<prophile>
joelteon wants to know if that means List.hd [] actually hangs indefinitely, or what happens
<prophile>
I take it does
<whitequark>
exception, at least in ocaml
<joelteon>
oh
<prophile>
ah, gotcha
<whitequark>
still doesn't return
<joelteon>
yeah, I should've thought of that.
<joelteon>
i'm pretty clever
<whitequark>
forall a. 'a also appears on rhs only in the type of call/cc
<prophile>
I feel like (something -> void)
<prophile>
would be a more obvious way of doing it
<whitequark>
yeah, but: say you have (if cond then foo else raise Exc)
<whitequark>
raise Exc never returns, so the fact that you can unify it with anything is convenient, type-safe and it just follows from HM
<prophile>
you could have a utility function for void -> a
<joelteon>
that's what Haskell does
<whitequark>
no
<joelteon>
I think whitequark said haskell is boring and mathy
<whitequark>
well
<whitequark>
if void means "never returns", then yes
<prophile>
void is the type with no values in it
<prophile>
so for any type, you can have a function to it from void
<whitequark>
'a in this context is treated in exactly same way: (forall a. anything -> 'a) is said to be "too generic to contain any values"
<joelteon>
that never returns
<prophile>
joelteon: well, it can never start, so to speak
<joelteon>
right
<prophile>
because you can never have an input to it
<joelteon>
so it certainly doesn't terminate
<joelteon>
why would you have a function like that?
<whitequark>
prophile: there's another consideration here.
<whitequark>
for example let's look at (let f () = f ())
<prophile>
joelteon: other than the curry-howard neatness, so that you can do things like have void on functions that don't terminate
<joelteon>
oh
<prophile>
whitequark: right
<whitequark>
as usual in HM, f first gets assigned the type of (unit -> 'a), which would be unified with something
<whitequark>
but there's nothing to unify it with, so it stays 'a
<prophile>
good point
<whitequark>
so on one hand, it all very nicely integrates with HM, but I swear this is a hack :D
<joelteon>
ok this conversation is utterly pointless
<prophile>
x^0 = 1 for all x
<joelteon>
what about 1/0
<whitequark>
oh?
<ec>
wait, did whitequark unignore joelteon?
<joelteon>
no
<joelteon>
that's why i stopped talking
<whitequark>
no
<joelteon>
it's more annoying than i thought
<prophile>
so for all T, void -> T is inhabited
<prophile>
that's a neat little property
<joelteon>
make them talk somewhere else, i keep tabbing back here when i see activity and remembering i can't participate
<prophile>
I'm not ignoring you joelteon
<joelteon>
i know
<joelteon>
but you didn't write the language
<joelteon>
it's an extra layer of abstraction i don't want to deal with
<prophile>
true dat
<prophile>
I'm also highly tempted to go for a walk
<joelteon>
yeah
<joelteon>
so this is doomed
<prophile>
but am currently thwarted by the lack of light
<ec>
what's opinion on those 400+ GHz “graphene” hybrid transistors?
<joelteon>
yeah, I guess I'll go to the gym, then
<joelteon>
my bike is a fucking disgrace
<ec>
I'm highly tempted to go to Costco and get Costco-sized pizza
<joelteon>
if i go over a rock, the chain detaches
<whitequark>
ec: link
<joelteon>
and the handlebars also loosened
<joelteon>
so now if I put any pressure on them they twist around so my hands are below my knees