00:00:34 <Sgeo> I just put Eliezer in charge
00:00:37 <ehird> dependent types are so sexy
00:01:03 * Sgeo returns to reality
00:01:19 <Sgeo> intuitionalistic type theory? o.O
00:03:01 <Sgeo> Since when is intuition valid in math? (note: I haven't actually read the article)
00:03:11 <coppro> intuition leads to valid math
00:03:22 <MissPiggy> well you can apply lots of common sense arguments
00:06:10 <oerjan> intuitionism is more about rejecting the parts of math that are _not_ intuitive, like the axiom of choice
00:07:23 <oerjan> and the law of excluded middle
00:08:28 -!- MigoMipo has quit (Remote host closed the connection).
00:09:55 <ehird> [00:00] <Sgeo> intuitionalistic type theory? o.O [00:02] <Sgeo> Since when is intuition valid in math? (note: I haven't actually read the article)
00:11:48 <coppro> The law of the excluded middle is usually intuitively correct
00:12:50 <ehird> excluded middle seems incredibly intuitive to me
00:12:54 <MissPiggy> yeah you can prove it for anything that has decidibility
00:12:55 <ehird> either something's right, or it isn't
00:13:03 <ehird> in our brains there isn't any
00:13:10 <ehird> "god doesn't exist, but god doesn't not exist!"
00:13:26 <pikhq> oerjan: I think it's just axiom of choice that gets people.
00:16:34 <MissPiggy> P \/ ~P is consistent but it's not really true
00:19:37 -!- coppro has quit (Quit: I am leaving. You are about to explode.).
00:19:41 <ehird> MissPiggy: why not?
00:19:49 <ehird> what is neither true nor false?
00:20:46 <ehird> what do you mean by that?
00:20:57 <ehird> they're false if you don't include them
00:21:12 <pikhq> They're true if you do include them.
00:21:24 <pikhq> (defined to be true, in fact)
00:22:27 <MissPiggy> if you don't include an (independent) axiom it's not provable but neither is it's negation
00:22:38 <ehird> MissPiggy: well yes, but provable != true
00:22:52 <ehird> the axiom is one of either true or false, you just can't know which
00:23:02 <ehird> and so it doesn't matter
00:23:03 <MissPiggy> I agree that provability is a subset of truth
00:23:27 <MissPiggy> but if you cannot prove something, then it is not acceptable to conclude that it is false
00:23:40 -!- coppro has joined.
00:24:12 <ehird> yes, I wasn't thinking properly
00:24:26 <MissPiggy> an idependent axiom is not necessarily true or false, because you can negate some of them -- such as the continuum hypothesis
00:24:32 <ehird> anyway, the axiom is either true or false; however, it is literally unknowable which it is, and since it never matters if it's true or false, it can be ignored entirely
00:24:36 <MissPiggy> or even that well founded set one (I think)
00:24:41 <MissPiggy> which gives you infinitely deep sets
00:25:07 <ehird> any non-included independent one
00:25:15 <ehird> anyway i'm just arguing that excluded middle is intuitive
00:25:16 <ehird> not that it's true
00:25:23 <ehird> i <3 constructivism
00:25:38 <ehird> and good look with forall a. Either a (a -> Void)
00:25:39 <MissPiggy> if we work in a theory T and there is an independent axiom A, then T+A and T+~A are both stronger than T
00:26:12 <pikhq> ehird: Yeah, it is quite intuitive.
00:26:20 <ehird> axiomatic :: a; axiomatic = error "Axioms are unquestionable"
00:26:37 <ehird> excludedMiddle :: forall a. Either a (a -> Void)
00:26:39 <ehird> excludedMiddle = axiomatic
00:26:53 <pikhq> To the point that it's such an obvious axiom for mathematic discussion that it's almost forgotten. :P
00:27:23 * MissPiggy still doesn't follow what ehird was saying
00:28:01 <MissPiggy> statements low on the arithmetic heirachy can be independent but /actually/ true
00:28:13 <ehird> let A be an independent axiom not in system S
00:28:33 <ehird> in S, either A or ~A; however, in S, one cannot know which it is, and it never matters
00:28:40 <ehird> therefore, the excluded middle stands
00:28:51 <MissPiggy> I don't know how you conclude this "in S, either A or ~A"?
00:28:57 <ehird> (in reality *whispers* you couldn't prove it to be either because it isn't, but it never ends up contradicting the excluded middle)
00:29:05 <ehird> (so it's effectively either in a nebulous way)
00:29:07 <MissPiggy> what if both S+A and S+~A are (equally) consistent?
00:29:09 <ehird> MissPiggy: given excluded middle
00:29:18 <ehird> S+A and S+~A are irrelevant in S
00:29:25 <MissPiggy> oh you're basicalyl arguing that assuming excluded middle then excluded middle? I agree with this
00:29:39 <ehird> you said excluded middle is consistent but not really true
00:29:52 <ehird> i'm arguing that it is "true" even from outside the system, when considering that system
00:31:16 -!- ehird has changed nick to alise.
00:31:25 <alise> forgot to change nick on reconnect :P
00:31:53 * alise tries modelling the dependent lambda calculus; she's helping me.
00:33:52 <coppro> first person in an ACTION?
00:34:59 <alise> She does all the work for you, and makes it just like you've got dependent types - almost.
00:35:05 <alise> She really does well to Haskell.
00:35:38 <alise> MissPiggy: isn't it awful that basically syntactic parts are holding up the representation of this? :(
00:35:48 <alise> we need some sort of awesome semanticity in the language of semanticity.
00:36:08 <coppro> now /me is really confused
00:36:37 <MissPiggy> it's utterly confusing when you start to think about everything as syntax..
00:36:46 <alise> coppro: She would help you not be confused. She is the one you should accept; she'd help.
00:37:07 <alise> She's the Strathclyde Haskell Enhancement, don't you know?
00:37:17 <alise> She has a homepage at http://personal.cis.strath.ac.uk/~conor/pub/she/.
00:37:34 <alise> MissPiggy: yeah, but I mean things like representing forall a. b
00:37:52 <alise> that's the thing that fucks up nice GADT representations of things
00:37:56 <alise> having to bind things to names then use them
00:38:07 <coppro> new rule: lower-case acronyms spelled the same as a pronoun should be banned
00:38:26 <MissPiggy> not having lambda in haskell is quite awful
00:38:35 <MissPiggy> lambda *in the type level* in haskell
00:39:04 <alise> coppro: She hates you for saying that.
00:39:08 <pikhq> MissPiggy: That's simple enough to fix.
00:39:15 <alise> I should name something "and".
00:39:21 <pikhq> Write a Template Haskell compiler from lambda to SK.
00:39:25 <pikhq> And define type-level SK.
00:39:36 <alise> We should use the best tool, and... And: it's the best way to get things done.
00:39:47 <alise> MissPiggy: yeah i *really* want type-level lambda
00:39:51 <alise> it'd be so easy to do this
00:39:52 <pikhq> The power of compile-time execution.
00:39:57 <alise> she should just let me do {\x -> ...} :(
00:40:53 <MissPiggy> we also need higher order unification though...
00:43:43 <alise> MissPiggy: basically what I want to write is
00:43:52 <alise> Forall :: (Type -> Type) -> Type
00:43:56 <alise> which works at the value-level
00:43:59 <alise> but at type-level? nope.
00:44:27 * alise wonders what she lifts that to
00:45:14 <alise> data SheSingType :: * -> * where{-# LINE 0 "Dunno.lhs" #-} SheWitForAll :: forall sha0. (SheChecks ((Type -> Type) ) sha0) => SheSingleton ((Type -> Type) ) sha0 -> SheSingType (SheTyForAll sha0){-# LINE 0 "Dunno.lhs" #-}
00:45:24 <alise> data SheTyArrow x1 x2 = SheTyArrow x1 x2{-# LINE 4 "foo.hs" #-}
00:45:26 <alise> pretty benign that
00:48:10 * Sgeo is watching Early Edition
00:49:15 <alise> MissPiggy: alas, she does not transmogrify (a -> b) into (* -> *)
00:50:26 <alise> a dependently-typed lambda calculus with names and some small sugar + optimisations for numbers and tuples and extracting the latter would make an excellent language to compile to
00:50:36 <alise> since you could just translate your types into its types, rather than check them yourself
00:52:42 <MissPiggy> a bit difficult to get good error messages though
00:52:59 <MissPiggy> oh I bet you could have some fun with Ziggeraut and that idea
00:54:21 <alise> MissPiggy: well it would have a feature where you would tag arbitrary expressions with strings
00:54:51 <alise> So you'd tag each atomic type in your lang to the composite type in the underlang, and if you have fancy composites that you compile away tag those too
00:55:00 <alise> (it'd give error reports in a convenient format to extract this stuff from)
00:55:05 <alise> some sexp-like thing
00:55:24 <alise> ugh, if I can't get this working very soon I'm doing it in agda
00:56:00 <alise> she doesn't really let you say (foo::Bar)
00:56:07 <alise> you can do pi (foo::Bar). but I think that's different in some way
00:56:08 <MissPiggy> why the fuck doesn't zsh read .profiele
00:56:17 <alise> it does but not if you have .zsh_profile
00:59:23 * alise writes what she wants to write then tries to coerce it so that she likes it (i'm going to call myself she because one, it'll result in even more being-named-she ambiguity and two, fuck you english language, I'll do what I want)
00:59:37 <alise> i'm fighting sexism in language or something
01:00:01 <alise> http://www.cs.virginia.edu/~evans/cs655/readings/purity.html is genius btw
01:00:47 <alise> I hate you, gedit. I WANT A NEW WINDOW, NOT A TAB
01:00:49 <alise> I HAVE A WINDOWING SYSTEM!
01:03:08 <alise> data Type where ForAll :: (Type -> Type) -> Type Arrow :: (a::Type) -> ID a -> ID TyTy -> Type -> Type TyVar :: ID a -> a TyTy :: Type
01:03:12 <alise> I want to write that.
01:03:22 <alise> data Term :: {Type} -> * where ID :: Term {Forall (\a -> Arrow a a)}
01:03:24 <alise> I want to be able to write that.
01:04:14 <MissPiggy> the problem with ForAll is that you can't unify it against anything nontrivial
01:04:21 <MissPiggy> because of haskell being very careful...
01:04:35 <alise> TyVar :: ID {a} -> {a}
01:04:39 <alise> is that actually valid in a GADT, I wonder?
01:04:43 <MissPiggy> (I've tried to do a non-She version of this before)
01:04:43 <alise> (desugars to just ID a -> a)
01:04:53 <alise> same thing as ID Type -> Type, heh
01:05:16 <MissPiggy> wow I have Coq Epigram and urweb installed
01:05:22 <alise> QUICK INSTALL AGDA
01:05:38 <MissPiggy> hmm maybe cabal will install agda for me
01:06:58 <alise> you actually do your type checking and evaluating and filling in and everything from inside emacs, feels very alive
01:07:05 <alise> http://pastie.org/812913.txt?key=7bkzz7vxkuiclztxsdof9q
01:07:07 <alise> note that you need to set it up with emacs
01:07:09 <alise> Here's what I want to be able to write.
01:07:10 <alise> it depends entirely on it
01:07:24 <alise> *ID {TyTy} -> Type
01:07:46 <alise> To do this with she, I need to figure out how to say (a::T).
01:08:17 -!- SimonRC has quit (Ping timeout: 246 seconds).
01:09:05 <alise> I don't think she lets you do pi (a :: T) from inside T :(
01:09:20 <alise> instance (SheChecks (pi (a :: Type). ID {a} ) sha0, SheChecks ( ID {TyTy} ) sha1, SheChecks ( Type ) sha2) => SheChecks (Type ) (SheTyArrow sha0 sha1 sha2) where sheTypes _ = SheWitArrow (sheTypes (SheProxy :: SheProxy (pi (a :: Type). ID {a} ) (sha0))) (sheTypes (SheProxy :: SheProxy ( ID {TyTy} ) (sha1))) (sheTypes (SheProxy :: SheProxy ( Type ) (sha2))){-# LINE 4 "foo.hs" #-}
01:09:45 <alise> Arrow :: forall a . SheSingleton ( Type) a -> ID (a) -> ID (SheTyTyTy) -> Type -> Type{-# LINE 16 "foo.hs" #-}
01:09:58 <alise> I want a bona-fide Type value at the value level
01:10:04 <alise> but I want it reflected in the type system too
01:10:08 <alise> and this is crossing the colon
01:10:09 <alise> which isn't allowed
01:11:36 -!- SimonRC has joined.
01:12:02 <oerjan> cross-colonization is dangerous
01:12:30 <alise> I think oerjan just renamed dependent types to a far more awesome name
01:13:00 <oerjan> it's apparently a medical term
01:13:46 <MissPiggy> is that when your colon gets angry
01:13:58 <alise> Maybe I should name my language Alise, it's a nice name
01:14:49 <alise> MissPiggy: is conor mcbride on irc?
01:19:44 <MissPiggy> which is good because he'd probably not get much done if he was
01:19:53 <alise> okay, I've decided that it's totally fruitless using haskell for this
01:20:03 <MissPiggy> he reads the dependent_types reddit though
01:20:32 * MissPiggy doesn't have agda installed yet because of an error
01:22:06 -!- cheater3 has joined.
01:22:59 <alise> now calling my language alise leads to the problem that the channel would be #alise but that's my nick and that would be strange,.
01:23:31 <coppro> the solution is to stop pretending to be a girl
01:23:44 <alise> who said i'm doing that now eh
01:23:51 <alise> PERHAPS MY MOTIVATION CHANGED, perhaps i just like this name
01:23:55 <coppro> also stop pretending to be Canadian
01:25:06 <alise> http://en.wikipedia.org/wiki/Alice_(programming_language) ok, alise would not be a good name for the language
01:25:19 <alise> oklopol: canadians say eh, eh
01:25:24 -!- cheater2 has quit (Ping timeout: 276 seconds).
01:25:39 <alise> MissPiggy: what error did you get?
01:25:53 <MissPiggy> cabal: cannot configure QuickCheck-2.1.0.3. It requires ghc -any
01:25:53 <MissPiggy> There is no available version of ghc that satisfies -any
01:26:48 <alise> pigworker = conor right?
01:26:57 <alise> MissPiggy: just checking. you have ghc right :D
01:29:42 <alise> cabal: cannot configure Agda-2.2.6. It requires base ==4.2.* && ==4.2.* For the dependency on base ==4.2.* && ==4.2.* there are these packages: base-4.2.0.0. However none of them are available. base-4.2.0.0 was excluded because of the top level dependency base -any
01:33:00 <alise> maybe i'll upgrade cabal-install
01:33:42 * Sgeo needs an ST monad tutorial
01:33:50 <alise> it's like io but only has iorefs
01:34:00 <Sgeo> Or something along the lines of how to hold onto state in Haskell
01:34:38 <MissPiggy> what do you mean hold onto State though?
01:34:47 <MissPiggy> mutable reference with O(1) update
01:36:35 <oerjan> Sgeo: ST is for temporarily using (real) mutable state inside a theoretically pure computation
01:37:59 <oerjan> if you want permanent mutable state you must use IO with IORef, MVar (thread safe) or maybe that TVar thing which i'm not sure about
01:38:03 -!- alise has quit (Ping timeout: 248 seconds).
01:38:41 <oerjan> and if you just want to _simulate_ state using pure computations, use State / StateT
01:39:22 <Sgeo> I want a nice tutorial on all of these
01:40:25 <oerjan> indeed, never seen a tutorial in my life </gross exaggeration>
01:42:14 -!- alise has joined.
01:42:37 <Gregor> Tutorials are just lies that the MAN uses to keep us down.
01:42:51 <oerjan> seems this one only has State of those, but it has many other monads: http://www.haskell.org/all_about_monads/html/index.html
01:57:17 <alise> MissPiggy: instead of a partial monad, would it be possible to have just an "infinite computation" monad?
01:58:20 <alise> well, partial lets you have things in-between
01:59:03 <alise> data Inf a = Further a (Inf a); bottom = Further bottom bottom -- I think
01:59:47 <oerjan> an infinite computation monad is just a partial monad where you cannot distinguish Further . Further from Further
02:00:06 <alise> oerjan: it's a partial monad where Later has some not-fully-computed value, and there is no Now
02:00:24 <oerjan> oh right no Now either
02:00:56 <oerjan> it's essentially opaque outside of runtime, then, like IO...
02:00:59 <augur> have you clarified your sex and/or gender to ehird?
02:01:34 <augur> i'd clarify your butter
02:01:40 <oerjan> until you clarify we shall have to refer to you by the generic pronoun (s)h/it
02:02:11 <alise> oerjan: not opaque
02:02:18 <alise> with a definition of the naturals you'd get
02:02:29 <alise> Further [] $ Further [1] $ Further [1,2] $ Futher [1,2,3] etc
02:02:37 <alise> Bottom would be Further ? $ Further ? $ Further ?
02:03:03 <alise> Length of an infinite list would be Further 0 $ Further 1 $ Further 2 $ ...
02:03:09 <oerjan> argh the question mark, my old nemesis
02:03:26 <alise> It's an actual question mark.
02:03:34 <oerjan> i know, i checked the logs
02:03:37 <alise> You *could* designate one value as the end valuie and leave the rest as placeholders to emulate Now/Later, so it's definitely equivalent.
02:03:49 <alise> With IO, for instance, you'd have an EndProgram event, and then just Nop, Nop, Nop forever,
02:03:55 <alise> (they'd never be looked at)
02:04:07 <alise> i.e. main_ = main >> exitSuccess
02:04:16 <alise> main_ = main >> exitSuccess >> main_
02:05:49 <alise> as alise I am getting speedier help in #haskell!
02:06:55 <oerjan> alise: hm this is possibly isomorphic to Reader Natural
02:07:21 <alise> right but not in a total language
02:07:41 <alise> MissPiggy: btw does agda allow something like foo :: Void -> a; foo _ = bottom?
02:07:49 <alise> if you have a Void you have bottom anyway, so you're not making anything worse
02:08:19 <MissPiggy> if you turn off the termination checker
02:09:15 <oerjan> data Void where bottom :: Void -> a
02:10:13 <oerjan> alise: foo x = case x of { }
02:10:24 <MissPiggy> that's the syntax to define it by "pattern match" on an empty type
02:11:07 <oerjan> that's intuitively correct, at least
02:11:38 <oerjan> MissPiggy: um you mean that foo () means the same thing?
02:11:46 <alise> Fun with the list monad: (| return ({[1..2]}, {[3..4]}) |)
02:12:18 <MissPiggy> oerjan, yeah (except that agda doesn't have case)
02:12:37 -!- Asztal has quit (Ping timeout: 265 seconds).
02:16:11 <alise> hmm... (| f {x} |) -> f <$> x, (| f {x} y |) -> join (f <$> x <*> return y)
02:18:01 <alise> (| f {g x} y {foo (| mab {z} |)} |) -> join (return f <*> g x <*> return y <*> foo (join (return mab <*> z)))
02:19:41 -!- SimonRC has quit (Ping timeout: 246 seconds).
02:20:06 <alise> oh, and (| x; y |) -> do (| x |); (| y |)
02:23:33 <alise> cat = (| putStr {getContents} |)
02:23:50 <alise> catLines = (| putStrLn {getLine}; catLines |)
02:24:19 <alise> MissPiggy: I wonder if you could make that table thing into the actual data type system of a functional lang
02:24:34 <alise> a gadt is shorthand for creating a table and adding some rows
02:24:43 <alise> functions are automatically turned into columns
02:25:04 <alise> (if they pattern match on the constructors; otherwise, they must be compositions of existing functions that do)
02:25:10 <alise> (and so don't need to be columns)
02:25:27 <alise> add some syntax for adding rows and voila
02:27:02 -!- SimonRC has joined.
02:27:20 <MissPiggy> but well it only defines a small class of functions
02:27:35 <alise> I don't see what you mean
02:28:01 <alise> also, it's ridiculous how much low hanging fruit there is in abstraction design
02:28:21 <alise> dependent types. a powerful module system ala ML. these tables. etc.
02:28:31 <alise> Yet nobody is putting them into their languages.
02:29:13 <MissPiggy> about time to start doing it I think :)
02:29:56 <alise> i'm so gonna have to hire some phds to write the compiler, though
02:30:18 <alise> proving the type system sound with all this stuff will be *way* out of my league for one :P
02:31:07 <MissPiggy> why not make a really simple dependent type core that has already been proved, and implement all your high language constructs in terms of it?
02:31:14 <MissPiggy> then you don't have to worry about consistency
02:31:32 <MissPiggy> this is the approach Coq takes (And the one Agda doesn't)
02:31:39 <alise> well, that's my plan, but some of the features would be really, really convoluted to compile
02:31:43 <alise> so need to be in the base language
02:31:46 <alise> and thus complicate things
02:31:58 <alise> also, because all the existing core systems suck, so i'd need to make a new one anyway :) :D
02:32:49 * alise gets another feature idea
02:33:01 <alise> a pair of brackets whose contents is interpreted according to a separate, extensible syntax
02:33:29 <alise> Well, you could have [[ /...regexp.../options ]], you could have [[ foo@bar.com ]], etc. etc. without polluting and worrying about clashes with the main syntax.
02:33:42 <alise> template haskell comes close to that, but not quite
02:35:45 <alise> (in one of its features)
02:36:44 <alise> (| email <penguinofthegods@gmail.com> {fileContents <~/message.txt>} |)
02:42:11 <alise> It'd be nice if there was a way to do symbolic computation without writing a parser in the lang
02:43:28 <coppro> just have a Symbolic type
02:43:34 <coppro> and use expression templates
02:43:52 <alise> whatever that is, it's probably a C++ abomination.
02:44:28 <coppro> Expression templates are when overloading is used to build up expressions in data
02:44:57 <coppro> e.g. x^2 might give some value which represents "x^2", which is exactly what you want in symbolic computation.
02:45:02 <alise> It's more the "any undefined value just sits there" thing.
02:45:46 <coppro> what about transcendental constants? For accurate math, they must be treated very much like unknowns
02:48:11 <alise> What I mean is, you need to coerce the language into, upon seeing "ilikebigbuttsandicannotlieyouothercreaturescantdeny", give it some value instead of barfing that it's not bound.
02:59:54 <Gregor> Time for GREGOR'S LANGUAGE CHALLENGE
03:00:07 <Gregor> Write a language with the following name:
03:00:11 <Gregor> ATTACK OF THE FLYING MONADS
03:01:10 <coppro> alise: That seems like a pretty easy feature to add
03:03:56 <alise> Adding arbitrary features is bad. Adding general constructs is good./
03:14:39 <alise> MissPiggy: would you believe i'm still at the "install agda" step in my dependent lc plan... >_<
03:15:19 <alise> and _this_ is why i have a grand os vision >:|
03:16:30 <alise> how to get agda in my lovely dream world: on their website, click a fancy link. it traces all the dependencies across the web, using things that basically amount to a set of type signatures to find dependencies that can be satisfied by multiple packages, and automatically integrating the latest versions, from decentralised sources, updatable, into the current value ecosystem.
03:18:26 <alise> yeah everything's called something else if you ignore pertinent words like decentralised, type signatures, and value ecosystem
03:18:49 <coppro> Debian supports decentralisation
03:19:03 <alise> if you believe your statement, you are not using the word i meant.
03:19:07 <coppro> don't even know what you mean by type signatures and value ecosystem
03:19:35 <alise> then perhaps you shouldn't make snarky comments about debian
03:19:44 <coppro> no, I just assume you're insane
03:19:57 <coppro> actually, you know what? I retract that
03:20:10 <alise> bitbucket :: a -> ()
03:20:15 <alise> > bitbucket coppro
03:20:35 <alise> coppro: perhaps slightly inappropriate given my current situation :P
03:20:43 <alise> retraction accepted, but i don't really mind
03:20:47 <oerjan> wait, we cannot claim we're all mad here any more? damn doctors.
03:20:59 <coppro> alise: "value ecosystem" turns up 0 relevant hits
03:21:13 <alise> so does your face.
03:21:21 <coppro> as for type signatures, I have no clue how that relates to packages
03:22:05 <alise> if you understood "value ecosystem" it would make more sense :P
03:22:25 <coppro> then explain it, because apparently you're the only one who does
03:23:00 <pikhq> Gregor: Attack of the Flying Monads, eh?
03:23:03 <alise> i'm sure others could infer it based on the component words, but imagine a smalltalk system; a living environment of objects, and that is all there is; there is no "running a file"
03:23:15 <alise> like that, but with functional-programming values instead of objects.
03:23:21 <Gregor> pikhq: No, ATTACK OF THE FLYING MONADS
03:23:27 <pikhq> Gregor: Definitely needs to use the function instance for monads as the only way to be Turing-complete.
03:23:36 <coppro> alise: I retract my retraction :P
03:23:39 <Sgeo> That (except for the functional bits) sounds like Unununium
03:23:48 <pikhq> (>>= is S, return is K)
03:23:49 <alise> coppro: yeah my system isn't unusable, i must be crazy
03:24:03 <pikhq> (... Erm, no. >>= is not S. XD.)
03:24:39 <pikhq> And ap is defined in terms of return and >>=...
03:24:58 <pikhq> So, >>= and return suffice for combinator calculus.
03:25:00 <coppro> alise: It's a pipe dream.
03:25:06 <alise> coppro: the os is called unununium
03:25:09 <alise> also, it's very much not
03:25:17 <alise> these techniques are actually simpler to implement than a traditional unix system
03:25:19 <oerjan> (f >>= g) x = g (f x) x
03:25:24 <alise> it's not one additional layer, it's one _less_ layer of separation
03:25:43 <pikhq> I just had a bit of a thinko.
03:25:49 <alise> the labelling of anything that is substantially different from the norm as a "pipe dream" is a very common technique to dismiss ideas for no reason whatsoever
03:25:52 <coppro> But it's one layer trying to abstract toom uch
03:25:59 <alise> you are wrong, and do not understand it
03:26:04 <coppro> occasionally pipe dreams work out
03:26:07 <alise> for one, smalltalk has existed since the 70s, and its implementation was _very_ simple
03:26:10 <alise> for two, run Squeak right now
03:26:15 <alise> you're using the exact thing I'm describing
03:26:23 <alise> for three, see Oberon OS. it fits on a floppy and does just this.
03:26:26 <alise> Squeak is an OS in a box
03:26:27 <alise> smalltalk is an os
03:26:31 <alise> it booted up the computer
03:26:34 <alise> squeak is descended from it
03:26:38 <alise> it's just in a window now
03:26:42 <pikhq> Smalltalk is one of the simpler OSes.
03:27:05 <pikhq> Since all that the "OS" is is a language runtime...
03:27:11 * Sgeo searches for Smalltalk.NET
03:27:16 <coppro> ah, I think I am misunderstanding
03:27:19 <pikhq> Everything else is just your library.
03:27:27 <alise> coppro: How did you interpret it?
03:28:09 <coppro> eh, I'm not really sure
03:28:18 * coppro tries to think it through
03:29:03 <alise> Believe me, I've thought about this at length; the bits you need to get an automatically persistent, typed, living ecosystem of values is actually incredibly minimal.
03:29:30 <oerjan> pikhq: >>= and return won't give you everything if you use haskell's type system though... no way to type the Y combinator
03:29:33 <alise> A living ecosystem of values is just a running program (ok, with the type information, etc. retained). Persistence? Orthogonal persistence takes a few hundred lines for a dumb version. A version ready for regular OS use? A few thousand lines.
03:29:42 <alise> And... well, that's it.
03:29:53 * coppro needs sleep, he thinks
03:30:02 <alise> The computer's memory becomes a disk cache, and the disk is full of values.
03:31:01 <coppro> okay, pretend I wasn't a part of this conversation. I think I was insane.
03:31:08 <alise> A lot of insanity.
03:31:13 <alise> what were you thinking? :P
03:31:33 <pikhq> oerjan: Just discussing ideas for ATTACK OF THE FLYING MONADS.
03:31:41 <pikhq> oerjan: Don't necessarily need Haskell's type system.
03:31:51 <coppro> alise: I'm not sure what I was thinking. Which is why I think I was insane.
03:32:25 <oerjan> pikhq: note that it says MONAD_S_. you cannot use just one ;D
03:32:36 <pikhq> oerjan: Yes, I know.
03:32:49 <pikhq> oerjan: I'm just saying the function instance should be the only thing making it TC. :P
03:33:25 <coppro> there's no reason we have to use the programming concept
03:33:29 <oerjan> hm maybe that reverse state monad would be something for getting fix-points...
03:33:59 <oerjan> then it can still be well-typed
03:34:13 <alise> i <3 the reverse state monad
03:34:38 <coppro> clearly we should be designing this off of music without resorting to chords
03:36:43 * coppro votes for Bach's rendition of the Ode to Joy
03:38:53 <oerjan> that would require some reverse state indeed, bach died before schiller was born (1750 vs. 1759)
03:40:42 <oerjan> hm a language based on time travelling anachronisms...
03:41:23 <oerjan> to quit the program, you need to get hitler eaten by a dinosaur.
03:41:50 <coppro> without causing an alternate world war to take its pace
03:42:24 <alise> wikihistory esolang
03:42:47 <alise> you have to do something in germany way back when to compute, but if anything stops hitler becoming an ebil nazi, the program is invalid
03:43:08 <alise> No, but I do have erectile dysfunction.
03:43:14 <alise> We all have our issues.
03:45:10 <Sgeo> Me: My email address is ********@gmail.com
03:45:16 <Sgeo> Other person: thats yahoo?
03:45:51 <coppro> alise: you're pulling off the female thing really badly
03:46:51 <alise> Sgeo: Just send the $500,000 so we can complete the transaction.
03:46:56 <alise> coppro: i know rite
03:47:04 <alise> coppro: well everyone knows i'm male in here so there's hardly any point
03:47:08 <alise> and the only other place i dwell is #haskell!
03:47:13 <coppro> but that's your own fault!
03:47:19 <Sgeo> Talking to someone who randomly came to a nearly dead chat
03:47:27 <alise> so the only affect of this is that i'm referring to myself as "she". well, when i remember.
03:47:46 <oerjan> alise: no wait, erectile dysfunction means you cannot be male, right
03:48:10 <Sgeo> The person invited me to private chat
03:48:19 <Sgeo> I was in another tab, but I accepted
03:48:24 <Sgeo> THat meant I couldn't see the main chat
03:48:53 <Sgeo> Just closed out of private chat... and apparently before I went into private chat, e said "Let's have sex"
03:51:43 <madbr> sex chat... usually that's hard because there's not many girls on IRC
03:52:02 <alise> it was probably in one of sgeo's endless obsessions^Wshitty 3d virtual-reality games from years ago.
03:52:13 <Sgeo> alise, you're psychic
03:52:40 <alise> actually the universe has shown a disturbing tendency to shape what i experience according to me recently
03:53:54 <pikhq> madbr: Though, if you're gay you shouldn't have *too* much trouble.
03:54:21 <pikhq> At least insofar as I can tell, there's more gay men than there are females on IRC. (in general)
03:54:37 <pikhq> If you're botsexual, then it's trivial.
03:55:49 <alise> coppro: i'm not ready for that kind of commitment.
03:56:01 <pikhq> coppro: /join #brainfuck
03:58:30 <Gregor> Sex chat is easy so long as you're not so damn picky :P
03:59:08 <alise> He knows this from extensive ... research,.
03:59:39 -!- Sgeo has quit (Ping timeout: 256 seconds).
03:59:57 <Gregor> If you can get off to chatting with what you assume is a sexy woman online, and some guy in Alabama can get off to pretending to be a sexy woman and chatting with you, then who's really harmed? :P
04:00:03 <pikhq> Clearly, everyone should only have sex chat with Egobot.
04:00:20 <Gregor> `echo I put on my robe and wizard's hat.
04:00:21 <HackEgo> I put on my robe and wizard's hat.
04:00:23 <alise> Gregor: THE IRC SERVER INBETWEEN
04:00:26 <alise> It knows everything
04:00:49 <madbr> ah, it has probably seen much worse
04:01:20 <alise> "I fling my dung-covered vomit into your urethra."
04:01:44 <Gregor> Urinal tract infections are SO SEXY.
04:06:19 <madbr> there was some guy in whatever other channel that had, like, all the fetishes
04:07:41 -!- alise_ has joined.
04:07:50 * coppro picks up the channel and sets it back on the rails
04:07:55 -!- alise has quit (Ping timeout: 248 seconds).
04:07:58 -!- alise_ has changed nick to alise.
04:08:11 -!- Sgeo has joined.
04:08:44 <Sgeo> That was screwed ip
04:09:35 <coppro> look, I already told you to stop being Canadian. Switching to a y doesn't count.
04:11:37 <madbr> There's no canada like french canada
04:12:52 <coppro> maple syrup is indeed delicious
04:13:21 <Sgeo> So is chapstick >.>
04:14:21 <alise> I'm beginning to suspect that chapstick is an euphemism for something else
04:14:38 <coppro> I'm going to assume it isn't
04:14:43 <madbr> everything in english is an euphemism for sex
04:16:26 <alise> madbr: including "english"?
04:16:34 <alise> Or how about ... discombobulated
04:16:43 <madbr> I'll give you english lessons
04:16:48 <oerjan> ooh, look at those bobules
04:17:03 <pikhq> madbr: No, just everything written by Shakespeare.
04:18:49 <Sgeo> http://tvtropes.org/pmwiki/pmwiki.php/Main/CountryMatters
04:19:47 <alise> I love that Ulysses quote.
04:22:07 <madbr> sgeo: heh, eventually we'll wear out "fuck" and have to switch to "cunt
04:27:59 <alise> i keep reading my name as aisle
04:28:17 <Sgeo> Pick up the phone booth and aisle?
04:28:44 <madbr> actually that might be a plan if you're a rapper that sells disks to 11 year olds by saying obscenities
04:47:19 <alise> amasses of obulence
04:49:29 <Gregor> I just want to pop open that stick of chapstick, pull out its fleshy inner core and rub it all over my lips.
04:49:34 <Gregor> Chapstick, folks. Chapstick.
04:51:06 <alise> My chapstick is tingling.
04:55:09 <oerjan> freud was wrong. all those people talking about penises are secretly thinking about chapsticks.
05:38:03 -!- Pthing has joined.
05:44:01 -!- jcp has quit (Ping timeout: 264 seconds).
05:45:19 -!- jcp has joined.
06:15:10 -!- oerjan has quit (Quit: Good night).
06:23:58 -!- madbr has quit (Quit: Radiateur).
06:39:41 <Sgeo> Most examples of using this particular SDK are C. This example is C++
06:41:34 <Sgeo> http://wiki.activeworlds.com/index.php?title=Aw_laser_beam
06:43:37 <Sgeo> At first, I forgot that C had structs, so I thought the whole Line thing wouldn't make sense
06:43:56 <Sgeo> Then I realized it does.. but it doesn't have the & pass-by-reference thing.. I think
06:45:14 <Sgeo> The & stuff is somewhat confusing, tbh
06:45:32 <Sgeo> I don't know why people think pointers are complicated. IMO, they make more sense
06:47:32 <coppro> References are used because operator overloading doesn't work with pointers
07:08:42 -!- coppro has quit (Ping timeout: 240 seconds).
07:11:14 -!- coppro has joined.
07:32:50 <coppro> alise: neat fact: I just discovered that a large portion of another online community thought I was female. No noticeable difference from my side.
07:59:59 -!- clog has quit (ended).
08:00:00 -!- clog has joined.
08:32:30 -!- jcp has quit (Remote host closed the connection).
08:34:33 -!- jcp has joined.
08:57:27 -!- MigoMipo has joined.
09:07:31 -!- gm|lap has quit (Quit: 2 hour UPS expired. Shutting down laptop.).
09:18:06 -!- MissPiggy has quit (Quit: Lost terminal).
09:21:39 -!- kar8nga has joined.
09:28:22 -!- BeholdMyGlory has joined.
09:29:03 -!- tombom has joined.
09:49:07 -!- jcp has quit (Remote host closed the connection).
10:35:02 -!- MigoMipo has quit (Remote host closed the connection).
10:37:19 -!- tombom_ has joined.
10:39:10 -!- tombom has quit (Ping timeout: 272 seconds).
11:10:49 * SimonRC just got a rather good fortune:
11:10:53 <SimonRC> To converse at the distance of the Indes by means of sympathetic contrivances
11:10:53 <SimonRC> may be as natural to future times as to us is a literary correspondence. -- Joseph Glanvill, 1661
11:24:30 -!- FireFly has joined.
11:58:08 -!- MizardX has joined.
12:20:31 -!- MigoMipo has joined.
13:35:04 -!- Pthing has quit (Remote host closed the connection).
13:48:43 -!- pax has joined.
13:53:02 -!- pax has quit (Ping timeout: 246 seconds).
13:57:29 -!- MizardX- has joined.
13:59:45 -!- MizardX has quit (Ping timeout: 256 seconds).
13:59:58 -!- MizardX- has changed nick to MizardX.
14:08:42 <alise> [07:32] <coppro> alise: neat fact: I just discovered that a large portion of another online community thought I was female. No noticeable difference from my side.
14:08:52 <alise> coppro: remember what I said about me seeming to shape the universe?
14:08:56 <alise> it's getting ridiculous lately.
14:09:30 <alise> i'm *almost* a multiverse solipsist (everyone has their own universe... except, I guess other people in it are "alive" just not the main alive guy for that person)
14:13:49 -!- kar8nga has quit (Remote host closed the connection).
14:18:23 -!- oerjan has joined.
14:20:02 <alise> oerjan: whatever curse you've put on me, stop it
14:20:58 <oerjan> wait, what? i was trying to put a curse on your doctors, not you. must have missed slightly.
14:23:37 <oerjan> also i was pondering more scientific plans. unfortunately they all involve first inventing a working teleport device.
14:28:13 <alise> the universe has been freaking me out since before that :p
14:28:48 <oerjan> also, synchronicities are supposed to increase drastically for _everyone_ as we approach 2012. don't you read the relevant new age literature, sheesh.
14:30:14 <alise> yes, but there's simply not enough space in the non-synchronicitious day for other people to have all theirs, too
14:30:36 <alise> if everyone was having these (I mean, assuming they're not just my imagination), mine wouldn't be so important as to affect the actual TV news
14:30:54 <oerjan> wait, you are affecting the TV news?
14:31:49 <oerjan> unless the TV news are mentioning you, note that the same news could easily be part of several people's synchronicities.
14:32:22 * Sgeo is curious as to what the news is
14:32:24 <alise> well, not as much recently but they *did* have a tendency to talk about things i'd recently thought about (not necessarily heard about; that would be Baader-Meinhof, but thought)
14:32:42 * oerjan has pondered this before, when _he_ felt the news were eerily coincident
14:33:30 -!- cheater3 has quit (Ping timeout: 248 seconds).
14:33:40 <alise> I'm pretty sure it's just the Baader-Meinhof phenomenon and a handful of everyday coincidences (it's not as if they're synchronicities about really obscure stuff)
14:36:29 <oerjan> well in my experience there are only a very few "big" synchronicities, and a tremendous onslaught of small ones, the frequency of which is affected by my personal mood.
14:37:20 <alise> In my experience, you're experiencing a rationality failure due to the tendency of the human mind to notice things that it has recently noticed and ignore those things it hasn't. :)
14:41:08 -!- Pthing has joined.
14:44:23 <oerjan> btw may i recommend the book "The Luck Factor"? it's investigating some of these things from a more scientific point of view.
14:44:55 <alise> from a 1-second google it's actually postulating that luck exists and some have it more than others?
14:45:08 <alise> so much for "scientific"
14:45:14 <oerjan> (well it's more in a popular science form)
14:45:32 <alise> "In this book Richard Wiseman, former magician turned"
14:45:42 <alise> james randi is the only one who can pull off that :P
14:46:54 <oerjan> it actually is not anywhere as non-scientific as it sounds. in fact it basically has your kind of outlook, but then notices (through scientific investigations) that you can _still_ affect your luck.
14:47:24 <oerjan> i.e. even _if_ it's all about perception, you can still affect your luck by changing it.
14:48:04 <alise> Only through working harder to do better (in ways that minutely change seemingly "random" outcomes) because you think you will...
14:48:24 <alise> Which isn't really changing your luck at all, luck would be affecting things you have no control over.
14:49:11 <oerjan> perhaps. this book is about the part you can control though, and why it's still important.
14:49:47 <alise> Well, I don't call things like that chance.
14:50:35 <oerjan> _i_ think there's more than that, of course.
14:51:03 <oerjan> but that book imho goes as far as you can _without_ leaving the scientific worldview
14:51:06 <alise> Many mathematicians seem to believe in the orbiting teapots, though I can't fathom why them specifically.
14:51:14 <oerjan> it was sort of gateway drug for me really
14:51:21 <alise> Maybe because their rational system doesn't say anything about the world.
14:51:28 <alise> So they don't make the connection...
14:52:58 <oerjan> whatever. i'll just have to wait for you to change your opinion ;D
14:55:39 <alise> That's unlikely; I've spent so much time - and in my formative years, too - thinking about this. I never was religious or superstitious - I identified as Christian but only because everyone else did, and *never* thought about it. Then I became an agnostic when I stopped telling people that, then, after much thought, a complete atheist. Then, a few years later, I took a long, hard look at it and concluded that rationality was the b
14:55:50 <alise> Although I'm a lazy slob and don't tend to follow my utilitarian aspirations.
14:56:56 <oerjan> i do not mean that you will change your opinion because you change your basic rationality. i don't think _i_ did, after all.
14:57:09 <alise> You believe in something entirely unfalsifiable.
14:57:22 <alise> That is irrational by definition.
14:57:40 * oerjan sets fire to alise's strawman
14:57:55 <alise> Then what do you believe?
14:59:10 <oerjan> i believe in synchronicities, the biggest of which have a strange tendency to show up when it is _really_ important that they do so.
14:59:46 <alise> Define synchronicities.
14:59:47 <Pthing> how do you spot a time when it's important to happen
14:59:56 <alise> Pthing: because it happened, obviously! :P
14:59:57 <oerjan> i guess _you_ have never been followed home by a three-legged black kitten when in a particularly self-destructive mood.
15:00:08 <alise> a kitten deciding to follow you
15:00:15 <alise> and it lost a leg because of some happening?
15:00:21 <alise> man, that's spoooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooky
15:01:52 <Pthing> surely there are instances where it could be really important one happens but it doesn't
15:01:52 <alise> if you say "whatever" as a response to something that's a pretty good indicator you're not able to make a rational argument about it
15:02:10 <oerjan> ok so i'm not rational.
15:02:42 <alise> That sure was easier to convince you of thaan it is for most. Are you sure you didn't already believe that?
15:03:01 <Pthing> jesus christ, you weren't convincing
15:03:14 <oerjan> i am not _intending_ to be convincing.
15:03:43 <alise> a second ago he was claiming he was rational.
15:03:49 <alise> anyway i didn't say i was convincing
15:03:53 <alise> that was not the word i used
15:04:06 <Pthing> "convince" is the word
15:07:35 <oerjan> ok i'm uncomfortable continuing this conversation. if it's because i'm irrational, so be it.
15:11:30 <oerjan> don't worry martians, the froghurt is cursed anyhow
15:13:42 <AnMaster> anyone know of a tool (for *nix) that renders a pdf (or ps file) and outputs it as one image per page
15:14:34 <AnMaster> alternative: anyone know of a tool to split up a multipage pdf into one file per page (I think ps2eps can be used then, and after that it would be easy to convert to a bitmap format)
15:19:54 -!- cheater2 has joined.
15:20:14 -!- oerjan has quit (Quit: Later).
15:30:11 <AnMaster> hm played with ghostscript's image backends
15:33:09 -!- MissPiggy has joined.
15:38:17 <AnMaster> oh hm you don't need to convert to ps for ghostscript it seems. Not that it is documented in man page that it accepts pdf (at least in the version I have here)
15:38:24 <AnMaster> and that gives antialiased output
15:44:16 <alise> MissPiggy: is the function Set -> Set reasonable that means "the set of all values not in the argument"? seems straying close to russell somehow, but it would be a cool function
15:45:41 <Ilari> alise: Either such function is relative to some universe (and then it would equivalent to set complement) or AFAIK the output will not be a set.
15:46:18 <fizzie> AnMaster: Well, it's a GNU thing; those aren't known for sensible man pages. The actual official documentation is pretty clear on PDF files.
15:46:27 <alise> Ilari: Well, it's relative to the type (āa.a).
15:47:01 <alise> MissPiggy: well for the typechecker it's easy
15:47:12 <alise> if the value is in the set we complemented, go all beepy like
15:47:27 <alise> you could construct a type of "everything you cannot `show` (as in Haskell show)" :D
15:47:58 * Sgeo is learning the joy of watching TED talks
15:47:59 <fizzie> AnMaster: And in general you have to say something like "-dTextAlphaBits=4 -dGraphicsAlphaBits=4" to get subsample antialiasing. (Can't say offhand why it'd happen by default if you pass in a PDF file.)
15:48:52 <alise> MissPiggy: i guess it's more useful to have complements
15:49:07 <alise> then you can just do (āa.a) - foo
15:49:10 <fizzie> AnMaster: (And incidentally, my version of the man page does mention the PDF support; starts with "-- Ghostscript, an interpreter of Adobe Systems' PostScript(tm) and Portable Document Format (PDF) languages."
15:49:13 <Ilari> alise: Any value not in set when invoked on empty set is truly everything. And that's proper class, not a set.
15:49:21 <alise> hmm, what uber-general concept can we apply to - to let us define it on sets? :-)
15:49:27 <alise> hmm... maybe sets are haskell-ish Nums
15:49:34 <alise> (+) :: Set -> Set -> Set, yes
15:49:52 <alise> (-) :: Set -> Set -> Set, yar
15:50:03 <Sgeo> In my Data Structures class, we made a fraction calculator in C++
15:50:05 <alise> (*) :: Set -> Set -> Set, that'd be a tuple
15:50:12 <Sgeo> Maybe I should make a similar calculator in Haskell
15:50:25 <alise> MissPiggy: Quick, what's set `div` set?!
15:50:34 <alise> (Not required for Num, but amusing to think about anyway.)
15:51:18 <Ilari> One property of sets is that for any set, there is strictly larger set.
15:53:03 <Ilari> More construcively: All sets have powerset, and that powerset is always strictly larger than the set itself.
15:53:48 <alise> There's no bigger set than (āa.a).
15:53:57 <alise> After all, it contains every single value...
15:54:33 * Sgeo guesses that the character he can't see is forall [inverted A]
15:54:44 <alise> Sgeo: It's flipped E.
15:54:52 <Ilari> alise: If there isn't anything bigger than it, it can't be a set, it is proper class.
15:55:07 <alise> In haskell, you would write it (forall a. a) because it overloads forall for existential quantification.
15:55:17 <alise> Ilari: Yes, but type theorists poop on set theory for breakfast.
15:57:09 <Ilari> Another funky feature: Sets with cardinality above Aleph-0 include undescribable elements.
15:57:57 <alise> Such is the strange world of the Curry-Howard isomorphism.
15:59:44 -!- kar8nga has joined.
15:59:47 <alise> (\(x::T). ...) -> (\x. (\x'. ...) (x::T)) if you have ::.
16:00:17 -!- Asztal has joined.
16:00:48 <alise> OTOH, (x::T) -> (\(x'::T). x') x if you have that. :P
16:05:02 -!- MissPigg1 has joined.
16:05:27 -!- MissPiggy has quit (Disconnected by services).
16:05:30 -!- MissPigg1 has changed nick to MissPiggy.
16:05:44 <alise> *Main> L (TyTy :-> (\(T a) -> a :-> (\_ -> a))) <interactive>:1:0: No instance for (Show (ID -> Term -> Term))
16:06:16 <alise> (That's (\...) :: (a::Set) -> a -> a)
16:08:19 <alise> I don't actually need to have separate Term and Set types.
16:08:49 <alise> L :: Term -> (Term -> Term) -> Term
16:08:51 <alise> (:->) :: Term -> (Term -> Term) -> Term
16:09:01 <alise> Whenever I see two things of the same type, I feel this intense urge to unify them.
16:09:11 <alise> But they're not the same :p
16:10:26 <alise> Starting to think that that function idea isn't so great, though, because then I can't, you know, show lambdas.
16:12:48 <alise> idL = L (A SetSet (A (N Top) (N (Dip Top)))) (N Top)
16:14:56 * Sgeo drinks a Red Bull shot
16:15:18 <Sgeo> It came free with a few hundred dollars worth of books
16:15:42 <alise> Let me guess, it's awful and terrible for you.
16:15:55 <Sgeo> My dad says that I better not buy this, because it's exactly the same as a cup of coffe, but more expensive
16:16:02 <alise> Don't let Ilari hear about this or you'll never stop hearing about sugar :-)
16:16:52 <Sgeo> He says if I want something convenient, there are pills
16:17:33 <alise> Or how about sleeping better and not needing things like that.
16:17:36 <alise> *Main> idL \((*) -> (t) -> dt). t
16:19:05 <Sgeo> If sugar's main issue is that it causes obesity or something, I don't see a problem
16:19:29 <alise> Destroys your liver
16:21:20 -!- jcp has joined.
16:26:37 <alise> Uh oh, my dependently-typed lambda calculus seems to require an infinite loop in typechecking.
16:29:18 * Sgeo does like the taste
16:29:24 <Sgeo> And I hate the taste of coffee
16:29:38 <alise> Drink tea. It has more caffeine.
16:30:14 <Sgeo> Drinking tea takes time
16:31:16 <alise> MissPiggy: HALP http://pastie.org/813531.txt?key=ahcwvmgdprki24beyw5gq
16:31:24 <alise> Sgeo: So does coffee
16:31:45 <alise> Anyway if you want a cheap boost the expense of your health feel free.
16:31:50 <Sgeo> Drinking this Red Bull shot took maybe a few seconds
16:31:50 <alise> , he said, while drinking cola.
16:31:55 <alise> MissPiggy: application
16:32:03 <alise> I would call it :$ but it's left-associative As God Intended
16:32:45 <alise> wait, rT isn't actually a function
16:32:52 <alise> so i can't do that
16:33:00 <alise> L :: Term -> Term -> Term A :: Term -> Term -> Term
16:33:08 <alise> maybe the second Term _should_ be a lambda
16:33:13 <alise> so that it's expressed as T -> (\x -> ...)
16:33:36 <alise> yeah but it'd actually be written as
16:33:38 <alise> not with a real lambda
16:33:40 <alise> but with an L term
16:33:59 <alise> idL = L (A SetSet (A (N Top) (N (Dip Top)))) (N Top)
16:34:03 <alise> (N is the variable stuff)
16:34:18 <alise> A, arrow, pushes a new variable and runs the code
16:34:26 <alise> so does L, so maybe A's second argument should be an L
16:37:14 <alise> In fact, I think I meant it to be an L.
16:37:39 <alise> MissPiggy: but the problem is, when I check the L in the A to make sure that it takes the right type of argument, and to make sure its result type is a Set, we run into the exact same code path
16:40:31 <alise> i was thinking i could rely on glorious laziness to bottom out in the end but i don't think so
16:41:22 <MissPiggy> for a well typed program you don't need to worry about evaluation order
16:42:37 <alise> yeah but my typechecker is sequential not lazy
16:43:05 <alise> the problem is that every type is, I think, infinite
16:43:11 <alise> every type has a type of the type and the typey type type
16:45:48 <alise> INFINITE DIMENSIONS OF THE COSMIC SOUL
16:45:57 <alise> ok lemme give you an example
16:46:40 <alise> note: a->b pushes the value of the a-typed value on the variable stack; top of var stack is t, second is dt, third ddt, etc
16:46:50 <alise> (\(* -> t -> dt) -> t) whatever
16:47:05 <alise> first we get the function's type
16:47:12 <alise> then whatever's typef
16:47:21 <alise> then we check the types match
16:47:27 <alise> we have to pass whatever to the (t -> dt) bit
16:47:36 <alise> which is a function, it needs to be typeofwhatever -> set
16:47:41 <alise> so we need to check it
16:47:45 <alise> check (that bit :. whatever)
16:47:50 <alise> ...but we're in the clause for (f :. x)
16:48:39 <alise> A's argument can't be an L
16:48:45 <alise> because that would cause an infinite nestingness
16:48:48 <alise> i may be able to solve this with my genius
16:48:52 <alise> i'm terribly clever
16:49:09 <alise> heh, to write my typechecker i need to write eval :/
16:49:45 <alise> fuck, at the end of this I'm going to write Term -> String
16:49:58 <alise> if there's one thing i'm getting out of this hellhole of coding
16:50:03 <alise> i'm gonna get some half-efficient code
16:50:13 <MissPiggy> http://sneezy.cs.nott.ac.uk/fplunch/weblog/?p=95
16:50:17 <alise> using `data ID = Top | Dip ID` for my names will make renaming and shit really terribly easy
16:50:39 <alise> well, that type is just de bruijn
16:50:47 <alise> maybe i should just use ints
16:50:53 <alise> MissPiggy: i can't use that technique, can't use haskell funcs
16:50:57 <alise> want to be able to `show` things nicely
16:51:08 <MissPiggy> you can quote it and show the quoted form
16:51:14 <MissPiggy> ro you could implement show on the functions
16:51:44 <alise> why do i need de bruijn stuff
16:51:47 <alise> if i have it as functions
16:52:50 <MissPiggy> well the syntax should be de bruijn, and the semantics is haskell functions
16:53:11 <MissPiggy> hmmm, does it even need to be de bruijn
16:53:18 <MissPiggy> maybe you are right and it doesn't matter
16:54:04 <alise> I need some sort of name to do the "pass the gensym"
16:54:21 <alise> so i guess it's best to keep it like that
16:54:43 <alise> you know what, I'm gonna write my evaluator first
16:54:45 <alise> then my typechecker
16:58:16 -!- MigoMipo has quit (Remote host closed the connection).
16:59:58 <alise> MissPiggy: that post confuses me
17:00:05 <alise> why does it have a separate type for evaluation?
17:01:23 <MissPiggy> suppose you have a syntax like: data Exp = Num Int | Var Ref | Add Exp Exp,
17:01:57 <alise> no variable binding :P
17:02:33 <MissPiggy> well the point is this, you have a type Syntax and another type Semantics,
17:02:44 <MissPiggy> eval :: Syntax -> Semantics, quote :: Semantics -> Syntax
17:02:51 <MissPiggy> now normalize = quote . eval :: Syntax -> Syntax,
17:03:20 <MissPiggy> the reason it gives you a normal form is because factoring through Semantics quotients out anything you don't care about
17:03:34 <alise> tell you what i'll just do it how the article says
17:03:45 <MissPiggy> for example if you have an associative binary operator (i.e. trees of a), you can use [a] as semantics, to quotient out associativity
17:03:46 <alise> but as far as i can tell Syntax = Semantics if I use haskell functions in the actual data types
17:04:08 <MissPiggy> then normalize ((p * q) * x * (y * z)) = p * (q * (x * (y * z)))
17:04:30 <MissPiggy> now if we use the semantic domain Sem = Sem -> Sem, we have a model of lambda calculus
17:04:41 <MissPiggy> and thats why it does beta normalization
17:05:22 <MissPiggy> (it's actually omre like data Sem = Sem (Sem -> Sem), oh and you need to be able to quote back out of it, so Sem = Sem (Sem -> Sem) | Var Ref)
17:05:54 <MissPiggy> if you use HOAS, syntax might be: data Syn = F (Syn -> Syn) | App Syn Syn | ...,
17:07:12 <alise> ok, so Sem is the untyped lambdas
17:07:19 <alise> and Syn is my dependently-typed language in its entirety
17:07:36 <alise> why not just keep track of vars with haskell arguments
17:08:19 <MissPiggy> the reason that I like ints for bound variables is you can do eval context (Var ref) = context ! ref
17:09:23 <alise> you don't need variable bindings
17:09:25 <alise> because Sem -> Sem
17:09:27 <alise> the first Sem gets a name
17:26:16 <MissPiggy> eval (N i) = Sem i ; eval (Add x y) = eval x <+> eval y
17:26:59 <MissPiggy> nf = quote . eval, now if x, y :: Syn are equal (like 1 + 4 is equal to 2 + 2 + 1 for example), so the property is:
17:27:27 <MissPiggy> === is extensional equality, and == is syntactic
17:27:57 <MissPiggy> so you can also do something like monoid simplification,
17:28:16 <MissPiggy> data Syn = Id | Var V | Op Syn Syn
17:28:37 <alise> ok, can i tell you the "issue" i'm having in code?
17:28:42 <MissPiggy> eval (Id) = [] ; eval (Var v) = [v] ; eval (Op x y) = eval x ++ eval y
17:29:08 <alise> data Syn = Lam (Syn -> Syn) | App Syn Syn
17:29:13 <MissPiggy> quote (Sem []) = Id ; quote (Sem (x:xs)) = Op x (quote (Sem xs))
17:29:16 <alise> one, what's the Sem for this? and two, when I quote it, how would I stringify it?
17:29:21 <alise> there's no "dummy gensyms" to pass
17:29:34 <MissPiggy> and you have nf = quote . eval, and nf normalizes out identity and associativity
17:30:08 <MissPiggy> yes Syn is a bit harder, we can build it up in two stages
17:30:38 <MissPiggy> eval (Lam f) = Sem (\x -> eval (f x))
17:30:47 <MissPiggy> eval (App f x) = eval f <$> eval x
17:31:07 <MissPiggy> now of course you can't quote this yet,
17:32:04 * Sgeo looks at some old Haskell code he wrote to try to get a taste for Haskell again
17:32:19 <alise> MissPiggy: that confuses me
17:32:59 <Sgeo> I can't believe I actually wrote
17:32:59 <MissPiggy> What exactly happened here is that we generalized the problem - in order to make recursion work on it
17:32:59 <Sgeo> show $ uncurry quad $ (\(x:y:[]) -> (x,y)) $ map read $ words line
17:33:06 * Sgeo should attempt to understand that
17:33:17 <MissPiggy> this is pretty much always a magic step, but it'll becme obvious in retrospect
17:33:19 <alise> MissPiggy: I'll have to think about this
17:33:24 <alise> maybe I should write the typechecker first :P
17:33:27 <MissPiggy> (same with induction proofs, when you do a magic generalization)
17:33:36 <alise> typechecker is Syn -> Maybe Syn (Syn includes types), not Sem right?
17:33:41 <alise> even though it involves evaluation at some point
17:33:45 <MissPiggy> anyway, the idea is that we generalized from CLOSED terms, to OPEN terms with N free vars,
17:34:03 <alise> i must be really dumb today :)
17:34:38 <MissPiggy> so if we have an term like OPEN 3, suppose the context is [oa, ob, oc]
17:34:39 <Sgeo> Ok, I understand what it does now :D
17:34:47 <Sgeo> I don't know if I could ever write it again though
17:34:53 <Sgeo> Plus, there's probably a more elegant way
17:35:02 <MissPiggy> and the term is maybe Sem (\x -> oa <$> x <$> ob)
17:36:42 <MissPiggy> the term is Sem (\x -> Neutral (NVar oa) <$> x <$> Neutral (NVar ob))
17:36:42 <MissPiggy> the recursion steps inside the binder and operates on "Neutral (NVar oa) <$> x <$> Neutral (NVar ob)" which is an open term with N+1 variables
17:36:48 <MissPiggy> of course you substitute x into say Neutral (NVar od)
17:37:29 <MissPiggy> once the lambda body is quoted you abstract it back out to get a syntax lambda term
17:38:25 <MissPiggy> ^ this is one bit where de bruijn syntax is slightly easier/nicer than HOAS I guess
17:41:13 <MissPiggy> You can also make quote type directed, so that it eta-expands
17:41:21 <MissPiggy> but that's just more tricky details :D
17:42:18 -!- MissPiggy has quit (Changing host).
17:42:18 -!- MissPiggy has joined.
17:43:53 * uorygl attempts to read Sgeo's code.
17:44:02 <uorygl> Kind of annoying how you have to read it from right to left.
17:44:19 <Sgeo> Probably I should paste the whole thing
17:44:26 <uorygl> Well, what does quad do?
17:44:49 <Sgeo> http://hpaste.org/fastcgi/hpaste.fcgi/view?id=17242
17:44:58 <alise> MissPiggy: isn't this more complicated than a syn->syn reductor :P
17:46:01 <alise> i've always wrote reducers like that and they seem "simple enough", perhaps slightly longer code but less semantic overhead i think
17:46:25 <uorygl> I guess that looks pretty simple.
17:47:07 <MissPiggy> I think the semantic domain way has better theoretical properties
17:47:59 <alise> but if you don't need them...
17:48:20 <uorygl> `translate Suomen kieli eli suomi kuuluu uralilaiseen kielikuntaan ja sen suomalais-ugrilaisen haaran itƤmerensuomalaisiin kieliin.
17:48:23 <HackEgo> The Finnish language, ie Finnish belongs to Uralic language family, and the Finno-Ugric branch of the Baltic-Finnish languages.
17:48:35 <alise> That's a very good automatic translation!
17:48:48 <uorygl> `translatefromto fi en eli
17:49:02 <uorygl> I guess ie is an English word now. :)
17:49:28 <uorygl> Yeah, I think that translation is pretty much perfect.
17:49:56 <uorygl> `translate kielikuntaan
17:49:58 <HackEgo> var sl_select, tl_select, web_sl_select, web_tl_select;var ctr, web_ctr, h;var tld = ".com";var sug_lab = "";var sug_thk = "";var sug_exp = "";var dhead = "Dictionary";var dmore = "View detailed dictionary";var tr_in = "Translating...";var isurl = "";var show_roman = "Show romanization";var
17:50:12 <uorygl> `translatefromto fi en kielikuntaan
17:50:51 <uorygl> `translatefromto fi en haaran
17:52:38 <uorygl> Okay, now that I mostly know what the individual words mean, I just have to re-read that sentence until it makes sense.
17:52:41 <pikhq> It would seem that my SKI interpreter, though much slower, does not have the severe memory leaks of the Lazy K interpreter.
17:53:20 <pikhq> In lazyk.cpp, rot13 takes gobs of memory.
17:53:28 <Deewiant> `translatefromto fi en kielikuntaankin
17:53:34 <pikhq> In my SKI interpreter, rot13 runs in constant space.
17:53:45 <pikhq> The power of garbage collection.
17:53:54 <Deewiant> `translatefromto fi en haarankin
17:54:19 <HackEgo> var sl_select, tl_select, web_sl_select, web_tl_select;var ctr, web_ctr, h;var tld = ".com";var sug_lab = "";var sug_thk = "";var sug_exp = "";var dhead = "Dictionary";var dmore = "View detailed dictionary";var tr_in = "Translating...";var isurl = "";var show_roman = "Show romanization";var
17:54:59 <uorygl> `translateto he Oy, this has a lovely bunch of coconuts in it!
17:55:01 <HackEgo> ×××, ×× ××××Ø× ×קה××× ×©× ×§×ק××”×× ××!
17:55:23 <uorygl> That looks like 'ad' in Greek.
17:56:33 <uorygl> `translateto he in it in it in it in it in it
17:57:26 <uorygl> `translatefromto fi en puhujia
17:57:39 <uorygl> `translatefromto fi en miljoonaa
17:58:00 <uorygl> `translatefromto fi en on noin viisi miljoonaa
17:59:14 <Deewiant> `translatefromto fi en ei ole noin viittƤ miljoonaakaan
17:59:15 <HackEgo> not even about five million
18:00:07 <uorygl> Does "Suomen kielen puhujia on noin viisi miljoonaa" literally mean "Finnish speakers are around five million"?
18:00:44 <uorygl> The way that you might say "We outnumber you: we are five, and you are only two", in a language other than English.
18:00:47 <Deewiant> As a literal translation, something like that, yeah.
18:00:53 <Deewiant> "There are around five million Finnish speakers"
18:01:51 <Deewiant> If you want the nonsense "Finnish speakers are around five million" literally translated: "Suomen kielen puhujat ovat noin viisi miljoonaa"
18:02:47 <uorygl> "Puhujia on" and "puhujat ovat" seem to be too many words for what they mean.
18:03:20 <uorygl> Not that I knew any Finnish at all before coming into this.
18:03:39 <uorygl> `translatefromto fi en puhujia on
18:03:41 <Deewiant> "Puhujia on x" == "there are x speakers"; "puhujat ovat x" == "[the?] speakers are x"
18:03:56 <Deewiant> `translatefromto fi en puhujia
18:03:59 <Deewiant> `translatefromto fi en puhujat
18:04:01 <Deewiant> `translatefromto fi en puhujia on
18:04:04 <Deewiant> `translatefromto fi en puhujat ovat
18:04:09 <Deewiant> `translatefromto fi en kaiuttimet
18:04:31 <uorygl> Are those the electric kind?
18:05:01 <uorygl> Anyway, yeah, I was forgetting that "puhuj-" is "speakers".
18:05:11 <uorygl> What's the citation form of that?
18:05:32 <uorygl> The form you would find in a dictionary.
18:05:54 <Deewiant> You'd probably find the singular, "puhuja".
18:06:01 <Deewiant> I'm still not quite sure what you're after.
18:06:18 <Deewiant> You might not even find that, you'd only find "to speak", "puhua".
18:06:29 <Deewiant> I'm not sure how dictionaries deal with this kind of thing.
18:06:40 <Deewiant> "Puhuja" is probably common enough by itself that you'd find it as well.
18:06:44 <uorygl> What case is "puhuja"? Nominative?
18:07:10 <Deewiant> You might like http://www.ling.helsinki.fi/~fkarlsso/genkau2.html
18:08:39 * uorygl looks up each of those words in a dictionary and memorizes their meanings individually. :P
18:09:37 <Deewiant> See, you'd only find the first in a dictionary :-P
18:10:25 <Deewiant> A verb equivalent, though the body text here is in Finnish as well: http://koti.mbnet.fi/henrihe/tiede/verbikaava.html
18:11:21 <uorygl> `translate HeistƤ suurin osa asuu Suomessa, mutta vanhoja suomenkielisiƤ vƤestƶryhmiƤ on Pohjois-Ruotsissa (meƤnkielen puhujat eli tornionlaaksolaiset), Norjassa (kveenit) sekƤ InkerissƤ, jossa suomen kieli on 1900-luvun mittaan suurimmaksi osaksi hƤvinnyt.
18:11:22 <Sgeo> "Why learning Haskell/Python makes you a worse programmer"
18:11:23 <HackEgo> The majority of them live in Finland, but the old Finnish-speaking population groups in northern Sweden (ie speakers MeƤnkieli Torne Valley people), Norway (Kvens) and Ingria, where the Finnish language is over the 1900s for the most part disappeared.
18:11:46 <pikhq> Sgeo: "Oh no it lets you write things more easily!"
18:11:47 <uorygl> Well, that translation doesn't really make sense.
18:12:08 <Sgeo> pikhq, it seems to be more that you get spoiled
18:12:10 <Sgeo> http://lukeplant.me.uk/blog/posts/why-learning-haskell-python-makes-you-a-worse-programmer/
18:12:29 <Deewiant> Seems fairly understandable to me
18:13:20 <uorygl> "The majority of them live in Finland, but the old groups where the Finnish language is over the 1900s for the most part disappeared."
18:13:27 <uorygl> Doesn't make much sense to me.
18:13:51 <Deewiant> You need to insert an "are" after "groups"
18:14:29 <Deewiant> And the thing at the end is trying to say that they have disappeared over the 1900s
18:14:55 <Deewiant> It's mostly the former issue that's confusing, IMO.
18:15:07 <pikhq> "Oh no it lets the computer focus on the trivial stuff"
18:16:15 <Sgeo> pikhq, it's "Oh no, I love Python and Haskell so much that I can't write C# code without getting depressed"
18:16:25 <uorygl> `translatefromto fi en vanhoja
18:16:54 <pikhq> Sgeo: So, he sucks at programming, and languages aren't going to change that.
18:16:57 <Deewiant> Finnish->English is so non-injective :-)
18:20:13 <uorygl> It's so convenient how no matter what channel I'm in, there are always suomen puhujia close at hand. :P
18:23:07 <Deewiant> Yeah, Finland's population is actually 5.5 billion, not million; we just like to stay undercover that way
18:40:54 <AnMaster> <fizzie> AnMaster: Well, it's a GNU thing; those aren't known for sensible man pages. The actual official documentation is pretty clear on PDF files. <-- well yes, that was how I found out about it
18:41:03 <alise> Sgeo: Ah yes, Luke Plant.
18:41:21 <AnMaster> <fizzie> AnMaster: And in general you have to say something like "-dTextAlphaBits=4 -dGraphicsAlphaBits=4" to get subsample antialiasing. (Can't say offhand why it'd happen by default if you pass in a PDF file.) <-- "not mentioned in man page" ;)
18:41:24 <alise> A creationist Christian.
18:41:33 <alise> Not someone to rely on to be anything other than a blithering moron.
18:41:57 <alise> I've read some of the drivel on his blog occasionally, and it's all that.
18:42:14 <Sgeo> I've found myself demotivated when writing C# >.>
18:42:23 <alise> So don't use shitty languages
18:44:21 <pikhq> C# is good at that.
18:44:34 <pikhq> It's not all that unique.
18:44:47 <pikhq> It's just an imperative language with objects.
18:45:59 <coppro> And we've got plenty of those
18:46:41 <coppro> In this case, alise is probably right
18:46:42 <alise> The Expression Problem may have solutions handling both rows and columns, but adding columns is far more valuable than rows.
18:46:49 <alise> So to hell with OOP.
18:46:56 <MissPiggy> oh still on the expression problem??
18:47:07 <MissPiggy> alise you know you can do BOTH in haskell?
18:47:11 -!- jcp has quit (Read error: Connection reset by peer).
18:47:29 <MissPiggy> like, data Exp = Num Int | Add Exp Exp | ..., then write functions on it
18:47:43 <alise> Okay: I WILL finish this dependent typer.
18:47:52 <alise> At least, before tomorrow; then I won't be able to.
18:47:54 <MissPiggy> or data Exp = Exp { eval :: Exp -> Int ; show :: Exp -> String, ... }, then write constructors for it
18:48:16 <MissPiggy> I got my record syntax wrong but just delete the "Exp ->"'s
18:48:23 -!- jcp has joined.
18:48:57 <coppro> alise won't be happy until he can make functional circuitry
18:50:47 <MissPiggy> alise I wrote a dependent type checkr once but the type system was inconsistent
18:51:11 <MissPiggy> but it didn't have subject reduction
18:51:20 <MissPiggy> anyway I realized that eventually, so that was fine
18:52:11 -!- alise has quit (Ping timeout: 248 seconds).
18:57:13 -!- alise has joined.
18:57:18 <alise> [18:56] * alise realises that infer x == specifiedType won't work if he has dependent types
18:57:28 * alise realises she has no idea how else to do this
18:57:38 <alise> i'm wayyy out of my league :D
18:57:48 <coppro> at least you got the pronoun right
18:58:13 <alise> 10:48:57 <coppro> alise won't be happy until he can make functional circuitry
18:58:19 <alise> no, the reduceron is fine :P
18:58:28 <alise> circuitry is functional
18:58:33 <alise> this sparks -> other thing
18:59:13 <alise> check' vs (L t _) = return t
18:59:21 <alise> after all, you wouldn't lie to me, would you?
18:59:31 <Sgeo> Why were my Chrome extensions all uninstalled?
18:59:38 <alise> Because you touch yourself at night.
19:02:12 <alise> Inferring variables will be hard, as in I haven't accounted for this.
19:02:39 <alise> But I have to keep track of variable's types.
19:02:59 <alise> Yes, and I'm not doing that, you see.
19:03:26 <alise> (A aT rT) <- check' vs f
19:03:31 <alise> okay, so I need to do it in the lambda-checking clause
19:04:00 <alise> check' vs (N x) = Nothing
19:04:02 <alise> shouldn't matter for now!
19:04:21 <alise> *Main> check SetSet
19:05:28 <alise> *Main> check idL Just (*) -> (t) -> dt *Main> check (idL :. idL) Nothing
19:05:30 <alise> Spot why I can't do that
19:07:19 <alise> so many interdependencies
19:08:12 <alise> no, idL :. typeofidL :. idL
19:08:29 <alise> de bruijn; t = 0, dt = 1, ddt = 2, etc
19:08:44 <alise> the value of the argument of that type is pushed for the RHS of ->
19:08:58 <alise> which incidentally means that evaluating your whole program in the typechecker is trivial :)
19:09:10 <alise> there's no IO so it doesn't matter
19:12:33 <alise> 10:47:29 <MissPiggy> like, data Exp = Num Int | Add Exp Exp | ..., then write functions on it
19:12:34 <alise> 10:47:54 <MissPiggy> or data Exp = Exp { eval :: Exp -> Int ; show :: Exp -> String, ... }, then write constructors for it
19:12:40 <alise> this + typeclasses might allow for both?
19:14:44 <MissPiggy> alise I don't want to say no but I dont see it
19:14:57 <alise> yeah i was just thinking that typeclasses solve... most problems
19:15:02 <alise> anyway your dependent solution doesn't require dependentness
19:15:07 <alise> type families = type-level functions, i bet you could do it with those
19:15:24 <MissPiggy> I am sure that my way make essential use of full spectrum dependent types
19:15:33 <alise> what was Snoc again?
19:15:47 <MissPiggy> Snoc was just an explanative device
19:16:06 <MissPiggy> you don't have to implement it that way, infact I think I realized a slightly better form
19:16:44 <alise> what was the better form?
19:16:47 <alise> also, I just meant the definition :P
19:17:08 -!- tombom__ has joined.
19:18:11 -!- Pthing has quit (Remote host closed the connection).
19:18:18 -!- tombom_ has quit (Ping timeout: 248 seconds).
19:19:51 <alise> MissPiggy: you know how the f gets the rest of the list?
19:19:57 <alise> what information does it need to make the ROW/COL decision?
19:20:01 <alise> the number of rows and the number of cols, right?
19:20:25 <alise> plus the types of the cols
19:20:32 <MissPiggy> well if you just have a matrix n m, then functions row : matrix n m -> vector n -> matrix n (S m)
19:20:42 <MissPiggy> and col : matrix n m -> vector m -> matrix (S n) m
19:20:50 <MissPiggy> I wonder if I got my n/m row/col right way around
19:20:59 <alise> I've forgotten the definition of snoc :(
19:23:31 <MissPiggy> "matrix : nat -> nat -> *" is a simplification though.. the real thing would be a bit more involved
19:23:45 <alise> so what would a table tarpit be, I wonder
19:23:50 <alise> do nested tables make sense?
19:24:27 <alise> if so, then obviously the whole program is one table, and there are columns that operate on the rows, which are tables; and the only atomic value is the empty table
19:25:30 -!- adam_d has joined.
19:26:48 <MissPiggy> nested table doesn't really mean anything
19:26:56 <MissPiggy> the only reason you'd need to think about multiple tables is:
19:27:03 <MissPiggy> either you have more than a 2D programming problems
19:27:04 <augur> MissPiggy: how been
19:27:20 <MissPiggy> or you have some kind of mututally recursive system of 2D programming problems
19:27:38 <MissPiggy> mutualy recursive infinite dimensional progarmming sounds hard thuogh
19:27:49 <MissPiggy> hey augur I was listening to the space flight remix
19:28:15 <augur> oooh right! the launch this morning
19:29:42 <MissPiggy> augur me and ehird solved the exeprssion problem using deptypes
19:29:53 <augur> been reading a bunch of some interesting grammar formalisms. improved the wikipages http://en.wikipedia.org/wiki/Indexed_grammar http://en.wikipedia.org/wiki/Combinatory_categorial_grammar http://en.wikipedia.org/wiki/Tree-adjoining_grammar and http://en.wikipedia.org/wiki/Weak_equivalence
19:30:05 <augur> AND i created the page http://en.wikipedia.org/wiki/Head_grammar
19:30:11 <MissPiggy> augur, I still need to get back to CCGs...
19:30:36 <augur> whats the expression problem?
19:31:05 <MissPiggy> augur you've done really good with these!!
19:31:25 <augur> well for all but the CCG one all i did was add the equivalency note, and some examples for LIG
19:31:30 <augur> the head grammar page is all new tho
19:33:13 <Sgeo> Wait, there's a new version of Haskell?
19:35:17 <alise> MissPiggy: link augur to my pastie about the expression problem
19:35:34 <alise> http://pastie.org/812459.txt?key=cadkhg4ho0qiceepz1a7w
19:37:56 <pikhq> Yeah; GHC doesn't implement it yet, though.
19:38:07 <pikhq> (won't be too long -- most of what's not done is syntax tweaks)
19:39:07 <augur> alise: interesting problem!
19:39:26 <alise> yeah MissPiggy came up with a nice solution
19:39:57 <augur> my solution would be, do like haskell does, but allow discontinuous definitions of function alternatives.
19:40:15 <augur> preprocess it to all be continuous, if desired.
19:41:24 <alise> augur: Anyway, that still doesn't let you add constructors to a data type.
19:42:07 <augur> but your link doesnt specify that as necessary, does it?
19:42:18 <alise> That's what adding a row is.
19:42:28 <augur> oh, right, because for haskell you'd have to have them all the same datatype
19:42:32 <alise> Anyway, here's the syntax I came up with: http://pastie.org/812720.txt?key=p9mayakdi0z2wka3vzwtq It would be implemented at compile-time; MissPiggy's solution is runtime.
19:42:44 <alise> The whole point is that they're the same type
19:48:04 -!- znerc has joined.
19:49:18 <augur> btw, guys, if anyone wants papers from JSTOR or ACM let me know
19:52:49 <augur> im also off to target. BYE
20:03:31 <alise> MissPiggy: you'd think that typechecking and evaluating the dependently-typed lambda calculus would be really simple...
20:03:45 <alise> it seems like one of those "inherent" concepts that should be really simple to express
20:04:14 <MissPiggy> there is a simple (dependently typed) lambda calculus, and that's quite easy to implement
20:05:41 <MissPiggy> well you know how types are equal if they are definitionally equal
20:06:13 <MissPiggy> one annoying thing is if you don't have eta conversion, then stuff like
20:06:29 <MissPiggy> exists Nat (\x -> P x) is not convertible with exists Nat P
20:06:38 <alise> f x :: Set(f) = (y::T) -> S, Set(x) = T, y = x, S
20:06:38 <MissPiggy> now that's just a minor annoyance,
20:06:42 <alise> \(x::T) -> ... :: S :: (x::T) -> S
20:06:43 -!- gm|lap has joined.
20:06:53 <alise> ^ the dependent lambda calculus i'm trying to implement
20:07:27 <MissPiggy> but there's more to be said about this which is sort of detailed
20:07:56 <alise> it's syntax :: type
20:07:58 <MissPiggy> T :: *, T' :: * |- (x::T) -> T' :: *
20:08:38 <alise> (x::T) -> S :: Set(T) = *, Set(x) = T, Set(S) = *, *
20:10:11 <alise> yeh i was just writing it quickly in the form it came into my head
20:11:13 <alise> data Syntax = Var Integer | App Syntax Syntax | Lambda Syntax Syntax | Arrow Syntax Syntax | Set
20:11:23 <alise> the semantics is just (Semantics -> Semantics), right?
20:11:29 <alise> or does it have Var Integer too
20:13:00 <alise> can my thingy type \x->x x?
20:13:07 <alise> there's no a = a -> b
20:13:31 <MissPiggy> Semantics = Semantics -> Semantics is a good first approximation
20:13:42 <MissPiggy> but to implement quote it needs to be fudged around a bit, nothing major
20:16:43 <alise> cons ā (Ī± ā ā
) ā (Ī² ā ā
) ā (Ī³ ā ā
) ā (Ī± ā Ī² ā Ī³) ā Ī³
20:17:17 <alise> cons ā· (Ī±ā·ā
) ā (Ī²ā·ā
) ā (Ī³ā·ā
) ā (Ī± ā Ī² ā Ī³) ā Ī³
20:17:21 <alise> Still think the latter looks nicer
20:17:35 <alise> cons : (Ī±:ā
) ā (Ī²:ā
) ā (Ī³:ā
) ā (Ī± ā Ī² ā Ī³) ā Ī³
20:17:37 <alise> looks good too, though
20:17:40 <alise> I think the last is best
20:20:02 <MissPiggy> lol those stars look awful in irssi
20:23:01 -!- oklopol has quit (Ping timeout: 264 seconds).
20:32:09 -!- MigoMipo has joined.
20:36:11 <gm|lap> eww. eww. eww. what kind of language is that
20:36:23 <gm|lap> GREEKS DID NOT MAKE THE MODERN COMPUTER
20:37:04 -!- MissPiggy has quit (Quit: Lost terminal).
20:41:07 -!- oerjan has joined.
20:45:43 -!- oklopol has joined.
20:46:21 <oerjan> almost no relation to prozac the bear
20:48:12 -!- MissPiggy has joined.
20:55:09 <alise> gm|lap: functional, bitch
20:55:34 <gm|lap> not very functional when you don't have loonycode
20:55:44 <oerjan> also, some mathematicians definitely were involved.
20:55:49 <alise> gm|lap: the 90s called
20:55:56 <alise> they want you to stop using windows
20:56:42 <gm|lap> it really depends on the situation as to whether using unicode is a good idea or not.
20:57:11 <gm|lap> here... uh, you'd have to whip up some special functions to deal with unicode chars like they were bytes or something
20:57:25 <gm|lap> as in, an fread of some sort.
20:57:26 <alise> gm|lap: Ah, you still think a string is a char *.
20:57:33 <alise> You still think C defines the world.
20:57:37 <gm|lap> here you'd use an int *
20:57:43 <alise> You still think stone-age computing rules over mathematics.
20:57:51 <oerjan> if C was good enough for the romans...
20:57:56 <alise> In short, you're the computer-science equivalent of a dinosaur.
20:58:12 <gm|lap> hey, at least i know how to code stuff which runs fast
20:58:20 <gm|lap> i usually don't, but nevertheless i can.
20:58:25 <alise> Except considering how fast computing changes, you're especially Ludditish.
20:58:29 <alise> Surely you've noticed the change?
20:58:31 * gm|lap opens up a can of ASM and spills it on your shirt
20:58:39 <oerjan> as in wildly successful, and survived for > 200 million years
20:58:54 <alise> Ha! You think hand-written asm written by _anyone_ other than a genius can beat modern C compilers?
20:58:57 <gm|lap> ASM will always be "potentially faster", by the way.
20:59:01 <alise> I thought you'd at least stop at C, a vaguely defensible position.
20:59:28 <alise> And apparently you think all the world's an imperative R/CISC architecture of the usual sort. Pay no attention to the Lisp Machines and Reducerons behind the curtain.
20:59:44 <gm|lap> i haven't seen ASM from many "modern C compilers" but usually they're bashing at memory
20:59:52 <alise> This may in fact end up being the most tedious two-way about computing I've ever seen.
20:59:54 <gm|lap> from the code I've seen
20:59:58 <alise> gm|lap: you are clearly ignorant of modern optimisation techniques
21:00:16 <alise> Good luck manually performing intense intraprocedural optimisation
21:01:02 <alise> I might be more polite if I didn't know there were so many like you.
21:01:06 <gm|lap> technically i'm someone who's kinda pissed at the fact that everyone's using 3D hardware in their demos, not because it's 3D hardware but because it's all closed and requires the use of specific libraries and stuff
21:01:22 <alise> Did I just miss some conversation or was that a non-sequitur?
21:01:30 <alise> MissPiggy: All your base is cool again?
21:01:37 <gm|lap> well, it may help you understand my thinking
21:01:57 <alise> I like open things too.
21:02:18 <gm|lap> a 4KB demo using libraries to run itself is technically cheating
21:02:23 <alise> oerjan: should I read Triangle and Robert?
21:02:39 <gm|lap> although if you want to be pedantic, i could whip up some code to turn 80x25 into mode 13
21:02:53 <alise> oerjan: but. so many comics
21:03:14 <oerjan> sure, but you're planning to live forever, aren't you
21:03:50 <alise> i'd like to, that doesn't mean i think it's going to happen :P
21:04:07 <gm|lap> you seem to be "oh yeah well this is futuristic so we'll just use it because it's the future". well, you wonder why people refer to "the good old days".
21:04:33 <alise> gm|lap: HA! You think functional programming, which is literally identical to mathematics and logic, is some new-fangled thing?
21:04:43 <alise> It's imperative programming that was the unfortunate blip in the history of calculation.
21:05:15 <gm|lap> i know that functional programming isn't insanely recent at all
21:05:32 <gm|lap> UTF-8 is definitely more recent than functional programming, though
21:05:39 <gm|lap> heck, you can even do OOP in ASM
21:05:48 <alise> But the symbols I am using are ancient.
21:05:50 <MissPiggy> can functional programming be liberated from the von noymann parradime?
21:05:56 <alise> Ugh, you know what, this really is the most tedious conversation I've had.
21:06:15 <oerjan> imperatives aren't new-fangled either, see kant
21:06:20 <alise> Especially as I'm returning to hell tomorrow, I don't feel the need to continue to perpetrate irritated boredom on myself.
21:07:03 <gm|lap> i know that the greek alphabet is ancient, but the current usual implementation requires you to either work on unicode chars or use a weird encoding
21:07:33 <alise> [21:07] == IGNORE Unknown command
21:07:36 <alise> Damn you, webchat.freenode.net.
21:08:46 <alise> So, I guess the answer to "will this ordeal soften me or harden me" is the latter, at least while it's still going on.
21:08:54 <alise> I'm being a wonderful asshole.
21:09:05 <gm|lap> yes, and my ignore list is wonderfully persistent.
21:09:32 <alise> He's been irritating for a few years now.
21:09:43 <gm|lap> alise: i don't remember you
21:09:47 <MissPiggy> it does feel like years, doesn't it?
21:09:50 <gm|lap> except from, ooh, a few days ago
21:09:51 <oerjan> always greasing up the place
21:09:59 <alise> gm|lap: i've been here a long while.
21:10:18 <alise> MissPiggy: it has been years; 2006, according to the wiki
21:10:32 <alise> oerjan: why did you fuck with it!
21:10:54 <gm|lap> what other names would you have used?
21:11:16 <alise> Johnathan, Omaha, Harpsichord, Robotic Overloard #3.9, Bob.
21:12:13 <gm|lap> ... don't really ring a bell
21:12:51 <alise> Also į į”į¢į£į¤į„į¦į§įØ.
21:15:10 <gm|lap> when i have a piece of paper, i deal with numbers.
21:15:17 <gm|lap> when i have a piece of code, i deal with bytes.
21:15:38 <alise> I thought you were using your wonderful ignore list.
21:15:50 <alise> Please do, I'm uninterested in your drivel and if it would stop you talking to me that would be great.
21:15:55 <gm|lap> yes, even though i code in languages which deal with all sorts of numbers, with and without decimal points
21:16:08 <gm|lap> hmm, i actually have some power here...
21:17:23 <alise> In a world... where one man... must face his demons...
21:17:30 <alise> THE POWER TO ANNOY
21:18:31 <gm|lap> on the other hand you have the power to be condescending
21:18:41 <pikhq> Wait, you deal with *bytes* in your programs?
21:18:46 <pikhq> I deal with *values*.
21:18:52 <alise> Maybe if my life was any better and you were any less idiotic I would not be trolling you. :)
21:19:06 <pikhq> Oh, and morphisms in the category Hask.
21:19:20 <gm|lap> i do actually deal with values, but when it comes to files, i have to deal with bytes
21:19:33 <alise> Files! Another wonderfully retarded blip in history.
21:20:02 <alise> a bunch; maybe i'll explain sometime when I'm not having fun with an idiot
21:20:03 <pikhq> MissPiggy: Made perfect sense when C was unusually high-level.
21:20:07 <gm|lap> i tried it, it's easy to break the GUI
21:20:11 <pikhq> That's been a few decades now.
21:20:13 <alise> MissPiggy: plan 9 is the closest to making files bearable
21:20:21 <alise> it basically makes them universal identifiers in tuple-space
21:20:36 <gm|lap> don't you mean plan 9 is the closes to making all bearables files?
21:20:36 <alise> It's easy to break the GUI.
21:20:46 <alise> Hey, now that was actually funny.
21:21:32 <pikhq> The thing is, files have no structure other than being a series of bytes. Implementing data structures in them is like manually implementing C semantics with an array and indices
21:21:41 <pikhq> That is to say, tedious and pointless.
21:22:06 <gm|lap> there's quite a difference between english and japanese, so to speak.
21:22:27 <MissPiggy> you want a "filesystem" that's actually storing data structures instead of just files in a tree
21:22:43 <MissPiggy> so it would be like a tree of trees instead of a tree of files?
21:22:46 <alise> even if files had no negatives I would oppose them for the simple fact that an orthogonally-persisted ecosystem of values is simply superior
21:22:57 <pikhq> I want a "filesystem" to just mean data structures that are persistent.
21:23:00 <alise> and allows you hierarchical, non-hierarchical, tagged, searched and everything organisation simply through creating data structures
21:23:19 <pikhq> I'd love for my IO to consist of "persist(foo)".
21:23:19 <alise> pikhq: Persistent data structures? Why, what redundancy!
21:23:27 <MissPiggy> it sounds very difficult to organize
21:23:32 <coppro> alise: what happened to amend?
21:23:41 <alise> MissPiggy: If you want a tree structure, like a symlinkless filesystem, just create it.
21:23:49 <alise> If you want symlinks, use references.
21:23:55 <alise> If you want a searchable pool, do it.
21:23:58 <gm|lap> alise: it's not going to make itself
21:24:11 <alise> gm|lap: That's why my main field of study is focused on making it.
21:24:36 <pikhq> MissPiggy: Are you familiar with Smalltalk?
21:24:46 <alise> An apology for the rather harsh bluntness, by the way; I'm grumpy right now.
21:26:24 <alise> I tend to confuse ignorance with wilful stupidity because I forget that not everyone really knows how possible, easy and flexible the superior system is, or even knows of the superior system.
21:27:13 <gm|lap> the question is, what am i confusing arrogance with?
21:27:57 <alise> Someone trying to distract himself.
21:28:00 -!- tombom_ has joined.
21:29:34 -!- MissPiggy has quit (Remote host closed the connection).
21:30:45 -!- alise has quit (Quit: Page closed).
21:31:05 <gm|lap> hmm... i think ruby 1.9.1 is comparable in speed with python 2.6.4
21:31:13 -!- tombom__ has quit (Ping timeout: 258 seconds).
21:31:21 <gm|lap> roughly half-speed ._>
21:31:27 <gm|lap> didn't notice the mixing rate
21:31:47 <gm|lap> 1.9.0 is pretty slow though
21:35:30 -!- MissPiggy has joined.
21:40:38 <gm|lap> there's a package in ubuntu called "sl"
21:40:52 <gm|lap> if you type sl accidentally, it suggests that you install it
21:41:03 <gm|lap> apt-cache search sl | grep ^sl gives us this:
21:41:04 <gm|lap> sl - Correct you if you type `sl' by mistake
21:41:50 <gm|lap> dude you should totally install it, it's awesome
21:42:00 <gm|lap> it makes an ascii train go across the screen
21:44:11 -!- alise has joined.
21:44:24 -!- adam_d has quit (Ping timeout: 256 seconds).
21:46:02 <alise> Testing, testing, one two three.
21:46:34 <alise> sl is just annoying IMO.
21:46:37 <alise> I never make that typo anyway.
21:47:00 <alise> The fact that there's no way to kill it without opening a new terminal makes it more of a life-ruiner rather than a stick.
21:47:18 <alise> Maybe there should be a carrot, getting ls right speeds up your system for a few minutes or something.
21:48:09 <gm|lap> apparently sl is short for "steam locomotive"
21:48:43 <alise> Yes; it's a rather terrible pun.
21:48:59 <alise> Damn, my XChat looks civilised.
21:51:12 <alise> http://imgur.com/CQv7v.png
21:51:20 <alise> I'd show the window borders, but apparently gnome-screenshot and scrot fail at compiz.
21:52:13 <alise> DejaVu Serif is actually a pretty nice serif.
21:56:35 <oerjan> well dejavu is nice but we've seen it all before
21:57:31 <Sgeo> Erm, button-tabs?
21:58:25 <alise> Beats a huge tree with only two lines.
21:59:29 <alise> URW Palladio L is also a nice font.
22:04:19 <alise> So, value-level (āa.b) is (Ī»a.b). What's value-level (āa.b)?
22:05:23 <alise> I guess you are right.
22:05:54 <alise> MissPiggy: What about the literal (āa.a)?
22:06:35 <alise> What does that translate to as a value?
22:06:40 <alise> If you replace exists with forall, that's id in value-land.
22:07:07 <MissPiggy> (a,a) sholud work, but also (a,a')
22:07:42 <alise> Right, but those would be specific as.
22:08:11 <alise> Perhaps my question simply makes no sense :P
22:11:44 <oerjan> well i understand that ghc implements exists a. TypeClass a => Whatever a as a tuple containing the typeclass instance and the value
22:12:28 <oerjan> or something close to that
22:12:58 <oerjan> but if there is no typeclass, only the value is necessary
22:13:14 <alise> Actually, (exists a. a) is 0 bits...
22:13:28 <alise> You don't need to store the value because the only information you can extract from it is that it exists.
22:14:03 <alise> Well, seq and unsafePerformIO are not "really Haskell". :)
22:14:10 <alise> "Really Haskell" is defined as the subset of Haskell that makes sense.
22:14:20 <alise> The committee is wrong.
22:14:50 <pikhq> alise: unsafePerformIO, FWIW, only exists as part of the FFI.
22:15:45 <oerjan> i think the new 2010 revision modifies that though
22:15:47 <alise> http://bennyhillifier.com/?id=mwDKMiAfxFE
22:16:00 <alise> Top of the two bots in the Google Tron AI competition, fighting.
22:16:01 <Sgeo> Where can I see the changes in 2010?
22:16:17 <alise> http://hackage.haskell.org/trac/haskell-prime/
22:17:12 <Sgeo> The link on that page seems broken
22:17:14 <MissPiggy> data Exists (T : *) (P : T -> *) where
22:17:23 <MissPiggy> Witness : (t : T) -> P t -> Exists T P
22:17:33 <alise> MissPiggy: Ah, dependent typists. Always writing everything in the language.
22:17:48 -!- tombom_ has quit (Quit: Leaving).
22:18:11 <alise> The Cult of Dependent Typists & their Honourable Languages Thereof, est. 1980
22:18:19 <alise> (I don't really know how old dependent types are.)
22:18:28 <alise> I wonder if dependent types have a nicer solution to the typeclass problem than typeclasses.
22:19:04 -!- MigoMipo has quit (Ping timeout: 240 seconds).
22:19:10 <oerjan> doesn't Agda supposedly have both?
22:19:29 <alise> I don't think there's any issue with having both.
22:19:33 <alise> I just don't really like typeclasses all that much.
22:19:50 <alise> I know that Ur does it with implicit module parameters matching a certain signature.
22:19:55 <alise> That's a nice solution.
22:20:03 <MissPiggy> it's sort of weird because I'm not sure if you can actually add typeclasses
22:20:25 <MissPiggy> I mean you can pass them explicitly but that probably doesn't count
22:20:26 <oerjan> oh right didn't oleg do something proving the equivalence of modules and type classes.
22:20:31 <alise> _+_ : {a:Set} -> {Num a} -> a -> a -> a
22:20:44 <alise> Num : Set -> ModuleSignatureThingy
22:20:51 <alise> Or something like that.
22:20:58 <oerjan> (functorial modules, presumably)
22:20:59 <alise> And the implementation:
22:21:25 <alise> _+_ {_} {n} x y = n._+_ x y
22:21:49 <Sgeo> alise, working link please?
22:21:57 -!- kar8nga has quit (Remote host closed the connection).
22:21:57 <MissPiggy> the problem with that is you still need the compiler to choose (ARBITRARITLY!!) a Num instance for a
22:21:59 <alise> To what? http://bennyhillifier.com/?id=mwDKMiAfxFE?
22:22:15 <alise> MissPiggy: same with values that belong to multiple sets in foralls!
22:22:18 <alise> It has to pick one!
22:22:26 <alise> Sgeo: http://bennyhillifier.com/?id=mwDKMiAfxFE
22:22:29 <alise> the final ? breaks it
22:22:35 <Sgeo> I do not consider "ou can see the list of [query:?status=new&status=assigned&status=reopened&state=accepted&milestone=Haskell+2010&order=priority changes in Haskell 2010]." to be helpful
22:22:52 <alise> just google haskell prime or w/e
22:23:08 <alise> MissPiggy: Well, it picks the most specific type it can infer, right?
22:23:14 <alise> Most specific set.
22:23:33 <alise> So all we need to define is how a Num-implementing module can be "more specific" than another and we're set.
22:23:48 <alise> Perhaps more functions explicitly implemented.
22:23:58 <alise> Or more concrete types.
22:24:06 <alise> If there are two equally-specific ones, you must manually specify one.
22:25:21 * oerjan finds a picture of oleg. i never thought of him as that old!
22:25:24 <MissPiggy> the whole thing about typeclasses is SYNTAx
22:25:36 <MissPiggy> and you can't add them without hacking the compiler
22:25:37 <alise> I imagine him as a 30-something guy
22:25:41 <alise> just being so fucking cool
22:25:49 <alise> no employer, he just has money, buys stuff, you know
22:25:50 <MissPiggy> and what's so good about them anyway, modules are probably better
22:25:53 <alise> but mostly just sits around, publishing
22:26:10 <oerjan> oh wait, that's another guy with the same!
22:26:10 <alise> MissPiggy: cayenne has no modules because its products (records) are powerful enough to serve as it
22:26:17 <alise> oerjan: I think he's a private fello
22:26:27 <oerjan> ("Oleg Kiselyov, director of Influenza Research Institute")
22:26:34 <alise> MissPiggy: so if modules are better than typeclasses
22:26:40 <alise> maybe we just need cayenne records and that's it!
22:27:22 * Sgeo is now an Early Edition addict
22:27:35 <alise> http://www.cs.chalmers.se/~augustss/cayenne/
22:27:40 <alise> hey, it's augustss
22:27:45 <alise> didn't know he did cayenne!!
22:28:00 <MissPiggy> doesn't he ? some kind of waterry thing
22:28:28 <alise> http://www.cs.chalmers.se/~augustss/cayenne/examples.html
22:28:32 <alise> cayenne's printf implementation is slick
22:28:34 <oerjan> heck wikipedia? "Oleg Kiselyov (born 11 January 1967) is a Russian handball player."
22:30:40 <alise> MissPiggy: I think cayenne records are basically haskell records
22:30:42 <alise> except automatically typed
22:30:57 <alise> like the type of {foo=3,bar=\a->a} is {foo::Int,bar::a->a} or whatever
22:31:10 <alise> also I realised something
22:31:16 <alise> my dependent LC doesn't have any way to extract an arrow
22:31:19 <alise> (the only composite type)
22:32:14 <alise> think I should add it? Maybe it could be a built-in function
22:32:36 <alise> destarr : * -> c -> (a -> b -> c) -> c
22:32:51 <MissPiggy> what does extract an arrow mean though?
22:33:27 <alise> I could add pattern matching, but that'd be the only thing it'd be useful for
22:34:53 <oerjan> hm this _might_ be him, http://www.flickr.com/photos/eelcovisser/283343950/ (it is in a computer scientists set)
22:35:21 <alise> Personal home page: Paul Kelly
22:35:21 <alise> Paul H J Kelly. Professor of Software Technology, Group Leader, Software Performance Optimisation · Department of Computing (map); Imperial College London ...
22:36:14 <oerjan> ok so you're sure? it was the only plausible picture on the first page of google hits for "oleg kiselyov"
22:36:19 <MissPiggy> it's his only t-shirt http://video.google.com/videoplay?docid=-7990603720514207956&ei=OkBvS7SkMovL-AbZwtHjBg&q=oleg+# :)
22:37:33 <oerjan> i guess that crushes my theory he is trying to keep his real appearance secret
22:38:12 <olsner> oerjan: do keep in mind that the pictures and videos are not necessarily of the actual oleg
22:38:37 <olsner> MissPiggy: indeed, just a puppet
22:39:26 <alise> ((Ī»:(ā
ā 0 ā 1). 0) (Ī»:(ā
ā 0 ā 1). 0)) (Ī»:(ā
ā 0 ā 1). 0)
22:39:31 <MissPiggy> there's another picture of Oleg on this http://www.angelfire.com/tx4/cus/people/index.html
22:40:12 <alise> Scheme / CL / Fortress
22:40:15 <alise> yeah, just ignore the whole Java thing
22:40:41 <oerjan> MissPiggy: i already knew about that one
22:40:43 <alise> ((Ī»:(ā
ā 0 ā 1). 0) (Ī»:(ā
ā 0 ā 1). 0)) (Ī»:(ā
ā 0 ā 1). 0)
22:40:46 <alise> does that make sense to you?
22:41:12 <oerjan> it was part of what started my conspiracy theory, after all
22:41:50 <alise> i can't do implicit arguments without full inferring can i :(
22:42:17 <alise> "lots" of work inferring
22:42:24 <alise> as opposed to some cheap trick
22:42:25 -!- adam_d has joined.
22:42:26 <MissPiggy> the best you can do is make a powerful algorithm that works well in normal situations
22:42:35 <alise> well, check does return the type
22:42:42 <MissPiggy> well there are some small classes of inference you can do in a principled way
22:42:56 <alise> all i care about is inferring type arguments :)
22:42:57 <MissPiggy> but it's very hard work.. and I think you probably need HOU to even get started
22:43:11 <alise> I think I could fake that since my typechecker returns a type it knows it is
22:43:36 <alise> ((((Ī»:(ā
ā 0 ā 1). 0) (ā
ā 0 ā 1)) (Ī»:(ā
ā 0 ā 1). 0)) (ā
ā 0 ā 1)) (Ī»:(ā
ā 0 ā 1). 0)
22:44:03 * alise writes cons out of sheer insanity
22:44:32 <alise> a:* -> b:* -> a -> b -> c:* -> (a -> b -> c) -> c
22:45:50 <alise> Lambda (Arrow Set (Arrow Set (Arrow (Var 1) (Arrow (Var 1) ...)))) $
22:45:50 <alise> Lambda (Arrow Set (Arrow (Var 1) (Arrow (Var 1) ...))) $
22:45:51 <alise> Lambda (Arrow (Var 1) (Arrow (Var 1) ...)) $
22:45:52 <alise> Lambda (Arrow (Var 1) ...) $
22:45:54 <alise> this is getting boring fast :P
22:46:17 <alise> not to mention confusing
22:46:44 <alise> okay so after c:*... what the fuck number is a
22:47:02 <alise> of course that'll change with the arguments of the function :D
22:50:06 <alise> foo3.hs:29:132: parse error on input `)'
22:50:42 <alise> Ī»:(ā
ā ā
ā 1 ā 1 ā ā
ā 4 ā 4 ā 2 ā 2). Ī»:(ā
ā 1 ā 1 ā ā
ā 4 ā 4 ā 2 ā 2). Ī»:(1 ā 1 ā ā
ā 4 ā 4 ā 2 ā 2). Ī»:(1 ā ā
ā 4 ā 4 ā 2 ā 2). Ī»:(ā
ā 4 ā 4 ā 2 ā 2). Ī»:(4 ā 4 ā 2 ā 2). ((0) (3)) (2)
22:51:01 <alise> i need more parens
22:51:08 <MissPiggy> write a function called --> that turns names into indices
22:51:18 <alise> and the opposite way, too
22:51:19 <Sgeo> Stupid broken A/V sync on this YouTube video
22:51:22 <alise> so I can see what the fuck will happen
22:51:26 <MissPiggy> so you can write ("x", T) --> "x" instead of T -> #0
22:51:32 <alise> Ī»:((ā
) ā (ā
) ā (1) ā (1) ā (ā
) ā ((4) ā (4) ā 2) ā 2). Ī»:((ā
) ā (1) ā (1) ā (ā
) ā ((4) ā (4) ā 2) ā 2). Ī»:((1) ā (1) ā (ā
) ā ((4) ā (4) ā 2) ā 2). Ī»:((1) ā (ā
) ā ((4) ā (4) ā 2) ā 2). Ī»:((ā
) ā ((4) ā (4) ā 2) ā 2). Ī»:(((4) ā (4) ā 2) ā 2). ((0) (3)) (2)
22:51:48 <alise> now in the sugar language I wrote over this, here's what it'll look like
22:53:03 <alise> cons : (Ī±:ā
) ā (Ī²:ā
) ā Ī± ā Ī² ā (Ī³:ā
) ā (Ī± ā Ī² ā Ī³) ā Ī³
22:53:12 <alise> cons _ _ x y _ f = f x y
22:53:32 <alise> MissPiggy: actually, if I define some standard representation for a tuple
22:53:47 <alise> then I can trivially infer an ((Ī±:ā
),Ī±) given an Ī±
22:53:56 <alise> simply because I must know the type already, since I'm doing typechecking
22:55:27 <alise> http://pastie.org/813947.txt?key=s3kxmqh9xb0pvxoycdqzpw
22:55:31 <alise> May I never have to write such a thing again
22:56:29 <alise> Dependently typed!
22:56:38 <alise> Pretty-printed (ha), it's
22:56:39 <alise> Ī»:((ā
) ā (ā
) ā (1) ā (1) ā (ā
) ā ((4) ā (4) ā 2) ā 2). Ī»:((ā
) ā (1) ā (1) ā (ā
) ā ((4) ā (4) ā 2) ā 2). Ī»:((1) ā (1) ā (ā
) ā ((4) ā (4) ā 2) ā 2). Ī»:((1) ā (ā
) ā ((4) ā (4) ā 2) ā 2). Ī»:((ā
) ā ((4) ā (4) ā 2) ā 2). Ī»:(((4) ā (4) ā 2) ā 2). ((0) (3)) (2)
22:56:43 <alise> MissPiggy: Because I have no other choice.
22:56:47 <alise> I have to curry because this is the LC.
22:57:00 <alise> But I have to specify the type of every function, because this is no-inferring, typed LC.
22:57:13 <alise> And I have to have additional Set arguments because this is the dependently-typed LC.
22:59:44 -!- adam_d_ has joined.
23:02:36 -!- adam_d has quit (Ping timeout: 256 seconds).
23:05:26 <alise> My variable names: Ī±Ī²Ī³Ī“ĪµĪ¶Ī·ĪøĪ¹ĪŗĪ¼Ī½Ī¾ĪæĻĻĻĻĻ
ĻĻĻĻ
23:05:50 <alise> I love the Greek alphabet. It's beautiful.
23:06:00 <MissPiggy> I should set it up so that alt-shift types greek
23:06:52 <alise> IMAL (In My Awesome Language), typing abcdefg... will automatically convert. :-)
23:07:44 <pikhq> alise: You and your derived-from-Egyptian scripts.
23:08:07 <alise> Unicode has up to quadruple prime :D
23:08:48 <alise> they don't compose together well, though
23:08:52 <alise> different numbers of primes
23:13:08 <alise> It has some stupidities, like the super/subscripts; it shouldn't be trying for a formatting vehicle.
23:13:14 <alise> *Main> System.IO.UTF8.putStrLn $ pretty idL
23:13:14 <alise> (Ī»:((Ī±:ā
) ā (Ī²:Ī±) ā Ī±))) Ī±. Ī±)
23:13:33 <alise> *Main> System.IO.UTF8.putStrLn $ pretty consL
23:13:33 <alise> (Ī»:((Ī±:ā
) ā (Ī²:ā
) ā (Ī³:Ī±) ā (Ī“:Ī²) ā (Īµ:ā
) ā (Ī¶:(Ī¶:Ī±) ā (Ī·:Ī²) ā Īµ))) ā Ī“))))))) Ī±. (Ī»:((Ī²:ā
) ā (Ī³:Ī±) ā (Ī“:Ī²) ā (Īµ:ā
) ā (Ī¶:(Ī¶:Ī±) ā (Ī·:Ī²) ā Īµ))) ā Ī“)))))) Ī². (Ī»:((Ī³:Ī±) ā (Ī“:Ī²) ā (Īµ:ā
) ā (Ī¶:(Ī¶:Ī±) ā (Ī·:Ī²) ā Īµ))) ā Ī“))))) Ī³. (Ī»:((Ī“:Ī²) ā (Īµ:ā
) ā (Ī¶:(Ī¶:Ī±) ā (Ī·:Ī²) ā Īµ))) ā Ī“)))) Ī“. (Ī»:((Īµ:ā
) ā (Ī¶:(Ī¶:Ī±) ā (Ī·:Ī²) ā Īµ))) ā Ī“))) Īµ
23:13:34 <alise> . (Ī»:((Ī¶:(Ī¶:Ī±) ā (Ī·:Ī²) ā Īµ))) ā Ī“)) Ī¶. Ī¶ Ī³ Ī“))))))
23:13:38 <alise> MissPiggy: I hope that clears things up for you.
23:14:03 <alise> "(Ī¶:(Ī¶:Ī±)" - bug or just plain awesomeness?
23:14:26 -!- SimonRC has quit (Ping timeout: 246 seconds).
23:14:38 <alise> It's because since you can't technically reference it from inside itself, it's free. :-)
23:16:04 <alise> MissPiggy: think I should change the type signatures to (Ī»(var:type):(result type). )? Not sure if that's actually any better :P
23:16:45 <alise> complains about v not being defined
23:17:43 <alise> *Main> System.IO.UTF8.putStrLn $ pretty consL
23:17:43 <alise> (Ī»:((Ī²:ā
) ā (Ī³:ā
) ā (Ī“:Ī³) ā (Īµ:Ī“) ā (Ī¶:ā
) ā (Ī·:(Īø:Ī“) ā (Ī¹:Īµ) ā Ī·))) ā Īµ))))))) Ī±. (Ī»:((Ī³:ā
) ā (Ī“:Ī³) ā (Īµ:Ī“) ā (Ī¶:ā
) ā (Ī·:(Īø:Ī“) ā (Ī¹:Īµ) ā Ī·))) ā Īµ)))))) Ī². (Ī»:((Ī“:Ī³) ā (Īµ:Ī“) ā (Ī¶:ā
) ā (Ī·:(Īø:Ī“) ā (Ī¹:Īµ) ā Ī·))) ā Īµ))))) Ī³. (Ī»:((Īµ:Ī“) ā (Ī¶:ā
) ā (Ī·:(Īø:Ī“) ā (Ī¹:Īµ) ā Ī·))) ā Īµ)))) Ī“. (Ī»:((Ī¶:ā
) ā (Ī·:(Īø:Ī“) ā (Ī¹:Īµ) ā Ī·))) ā Īµ))) Īµ
23:17:43 <alise> . (Ī»:((Ī·:(Īø:Ī“) ā (Ī¹:Īµ) ā Ī·))) ā Īµ)) Ī¶. Ī¶ Ī³ Ī“))))))
23:17:48 <alise> MissPiggy: It's simple, really.
23:17:59 <alise> I pity the foo that has to debug their code generator for this
23:19:12 <alise> MissPiggy: it would probably help if I didn't try and avoid types and variables clashing (same list) :)
23:21:05 -!- MizardX- has joined.
23:21:44 <alise> *Main> System.IO.UTF8.putStrLn $ pretty (Arrow (Arrow Set Set) (Arrow Set Set))
23:21:45 <alise> (Ī± : (Ī² : ā
) ā ā
) ā (Ī² : ā
) ā ā
23:21:49 <alise> I should probably retain used variables
23:22:18 <alise> this could do with becoming monadic
23:23:10 <oerjan> you mean to make it even more incomprehensible?
23:24:37 -!- MizardX has quit (Ping timeout: 260 seconds).
23:24:38 -!- SimonRC has joined.
23:25:04 -!- MizardX- has changed nick to MizardX.
23:25:16 -!- znerc has quit (Remote host closed the connection).
23:29:10 <MissPiggy> have you raed peter morris' work on universe of strictly positive typs
23:34:46 * alise will implement a new feature in the prettifier
23:34:56 <alise> arguments whose values are ignored in the type will be just shown as their type
23:36:32 -!- jcp has quit (Quit: I will do anything (almost) for a new router.).
23:45:19 -!- FireFly has quit (Quit: Leaving).
23:51:54 <alise> *Main> System.IO.UTF8.putStrLn $ pretty idL
23:51:54 <alise> (Ī»(Ī±:ā
) : (Ī± : Ī±) ā *** Exception: List.genericIndex: index too large.
23:57:57 -!- jcp has joined.