00:00:34 I just put Eliezer in charge 00:00:37 dependent types are so sexy 00:01:03 * Sgeo returns to reality 00:01:19 intuitionalistic type theory? o.O 00:02:05 what about it?? 00:03:01 Since when is intuition valid in math? (note: I haven't actually read the article) 00:03:08 haha 00:03:11 intuition leads to valid math 00:03:22 well you can apply lots of common sense arguments 00:06:10 intuitionism is more about rejecting the parts of math that are _not_ intuitive, like the axiom of choice 00:06:16 afaiu 00:07:23 and the law of excluded middle 00:08:28 -!- MigoMipo has quit (Remote host closed the connection). 00:09:55 [00:00] intuitionalistic type theory? o.O [00:02] Since when is intuition valid in math? (note: I haven't actually read the article) 00:09:57 * ehird facepalms 00:11:48 The law of the excluded middle is usually intuitively correct 00:12:50 excluded middle seems incredibly intuitive to me 00:12:54 yeah you can prove it for anything that has decidibility 00:12:55 either something's right, or it isn't 00:12:57 lol 00:13:03 in our brains there isn't any 00:13:10 "god doesn't exist, but god doesn't not exist!" 00:13:26 oerjan: I think it's just axiom of choice that gets people. 00:16:34 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 MissPiggy: why not? 00:19:49 what is neither true nor false? 00:20:01 any independent axiom 00:20:46 what do you mean by that? 00:20:57 they're false if you don't include them 00:21:12 They're true if you do include them. 00:21:24 (defined to be true, in fact) 00:22:25 of course 00:22:27 if you don't include an (independent) axiom it's not provable but neither is it's negation 00:22:38 MissPiggy: well yes, but provable != true 00:22:52 the axiom is one of either true or false, you just can't know which 00:23:02 and so it doesn't matter 00:23:03 I agree that provability is a subset of truth 00:23:27 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 yes, I wasn't thinking properly 00:24:26 an idependent axiom is not necessarily true or false, because you can negate some of them -- such as the continuum hypothesis 00:24:32 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 or even that well founded set one (I think) 00:24:41 which gives you infinitely deep sets 00:24:52 which axiom? 00:25:07 any non-included independent one 00:25:15 anyway i'm just arguing that excluded middle is intuitive 00:25:16 not that it's true 00:25:23 i <3 constructivism 00:25:38 and good look with forall a. Either a (a -> Void) 00:25:39 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:25:41 *luck 00:26:12 ehird: Yeah, it is quite intuitive. 00:26:20 axiomatic :: a; axiomatic = error "Axioms are unquestionable" 00:26:37 excludedMiddle :: forall a. Either a (a -> Void) 00:26:39 excludedMiddle = axiomatic 00:26:53 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 statements low on the arithmetic heirachy can be independent but /actually/ true 00:28:13 let A be an independent axiom not in system S 00:28:33 in S, either A or ~A; however, in S, one cannot know which it is, and it never matters 00:28:40 therefore, the excluded middle stands 00:28:51 I don't know how you conclude this "in S, either A or ~A"? 00:28:57 (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 (so it's effectively either in a nebulous way) 00:29:07 what if both S+A and S+~A are (equally) consistent? 00:29:09 MissPiggy: given excluded middle 00:29:18 S+A and S+~A are irrelevant in S 00:29:25 oh you're basicalyl arguing that assuming excluded middle then excluded middle? I agree with this 00:29:31 well, no 00:29:39 you said excluded middle is consistent but not really true 00:29:44 yes 00:29:52 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 forgot to change nick on reconnect :P 00:31:53 * alise tries modelling the dependent lambda calculus; she's helping me. 00:33:52 first person in an ACTION? 00:34:14 lol 00:34:21 She is a haskell enhancement 00:34:37 She's lovely. 00:34:59 She does all the work for you, and makes it just like you've got dependent types - almost. 00:35:05 She really does well to Haskell. 00:35:38 MissPiggy: isn't it awful that basically syntactic parts are holding up the representation of this? :( 00:35:48 we need some sort of awesome semanticity in the language of semanticity. 00:36:08 now /me is really confused 00:36:18 alise everything is syntax :P 00:36:22 everything you write down anyway 00:36:37 it's utterly confusing when you start to think about everything as syntax.. 00:36:46 coppro: She would help you not be confused. She is the one you should accept; she'd help. 00:37:04 who is the 'she'? 00:37:07 She's the Strathclyde Haskell Enhancement, don't you know? 00:37:17 She has a homepage at http://personal.cis.strath.ac.uk/~conor/pub/she/. 00:37:34 MissPiggy: yeah, but I mean things like representing forall a. b 00:37:35 ah 00:37:52 that's the thing that fucks up nice GADT representations of things 00:37:56 having to bind things to names then use them 00:38:07 new rule: lower-case acronyms spelled the same as a pronoun should be banned 00:38:08 oh I'm not sure what you mean 00:38:26 not having lambda in haskell is quite awful 00:38:35 lambda *in the type level* in haskell 00:39:04 coppro: She hates you for saying that. 00:39:08 MissPiggy: That's simple enough to fix. 00:39:14 is it? 00:39:15 I should name something "and". 00:39:21 Write a Template Haskell compiler from lambda to SK. 00:39:25 And define type-level SK. 00:39:29 Voila. 00:39:30 hmm 00:39:36 We should use the best tool, and... And: it's the best way to get things done. 00:39:47 MissPiggy: yeah i *really* want type-level lambda 00:39:51 it'd be so easy to do this 00:39:52 The power of compile-time execution. 00:39:57 she should just let me do {\x -> ...} :( 00:40:30 alise do it! based on pikhqs idea 00:40:44 oh 00:40:53 we also need higher order unification though... 00:41:09 lol 00:43:32 a unified world order 00:43:43 MissPiggy: basically what I want to write is 00:43:52 Forall :: (Type -> Type) -> Type 00:43:56 which works at the value-level 00:43:59 but at type-level? nope. 00:44:27 * alise wonders what she lifts that to 00:45:14 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:15 yikes 00:45:22 but uh 00:45:24 data SheTyArrow x1 x2 = SheTyArrow x1 x2{-# LINE 4 "foo.hs" #-} 00:45:26 pretty benign that 00:45:33 (shitty arrow) 00:48:10 * Sgeo is watching Early Edition 00:49:15 MissPiggy: alas, she does not transmogrify (a -> b) into (* -> *) 00:50:26 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 since you could just translate your types into its types, rather than check them yourself 00:52:35 yeah 00:52:42 a bit difficult to get good error messages though 00:52:59 oh I bet you could have some fun with Ziggeraut and that idea 00:54:21 MissPiggy: well it would have a feature where you would tag arbitrary expressions with strings 00:54:51 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 (it'd give error reports in a convenient format to extract this stuff from) 00:55:05 some sexp-like thing 00:55:24 ugh, if I can't get this working very soon I'm doing it in agda 00:56:00 she doesn't really let you say (foo::Bar) 00:56:07 you can do pi (foo::Bar). but I think that's different in some way 00:56:08 why the fuck doesn't zsh read .profiele 00:56:17 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 i'm fighting sexism in language or something 00:59:47 linguistics! 00:59:49 MissPiggy: speeling? 01:00:01 http://www.cs.virginia.edu/~evans/cs655/readings/purity.html is genius btw 01:00:47 I hate you, gedit. I WANT A NEW WINDOW, NOT A TAB 01:00:49 I HAVE A WINDOWING SYSTEM! 01:03:08 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 I want to write that. 01:03:22 data Term :: {Type} -> * where ID :: Term {Forall (\a -> Arrow a a)} 01:03:24 I want to be able to write that. 01:04:14 the problem with ForAll is that you can't unify it against anything nontrivial 01:04:21 because of haskell being very careful... 01:04:35 TyVar :: ID {a} -> {a} 01:04:39 is that actually valid in a GADT, I wonder? 01:04:43 (I've tried to do a non-She version of this before) 01:04:43 (desugars to just ID a -> a) 01:04:50 er, wait 01:04:53 same thing as ID Type -> Type, heh 01:05:16 wow I have Coq Epigram and urweb installed 01:05:22 QUICK INSTALL AGDA 01:05:31 heh I should do 01:05:38 hmm maybe cabal will install agda for me 01:06:56 it does 01:06:58 you actually do your type checking and evaluating and filling in and everything from inside emacs, feels very alive 01:07:05 http://pastie.org/812913.txt?key=7bkzz7vxkuiclztxsdof9q 01:07:07 note that you need to set it up with emacs 01:07:09 Here's what I want to be able to write. 01:07:10 it depends entirely on it 01:07:24 *ID {TyTy} -> Type 01:07:46 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 I don't think she lets you do pi (a :: T) from inside T :( 01:09:20 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:21 sigh 01:09:45 Arrow :: forall a . SheSingleton ( Type) a -> ID (a) -> ID (SheTyTyTy) -> Type -> Type{-# LINE 16 "foo.hs" #-} 01:09:47 the problem is 01:09:58 I want a bona-fide Type value at the value level 01:10:04 but I want it reflected in the type system too 01:10:08 and this is crossing the colon 01:10:09 which isn't allowed 01:11:36 -!- SimonRC has joined. 01:12:02 cross-colonization is dangerous 01:12:28 :D 01:12:30 I think oerjan just renamed dependent types to a far more awesome name 01:13:00 it's apparently a medical term 01:13:46 is that when your colon gets angry 01:13:52 >_< 01:13:58 Maybe I should name my language Alise, it's a nice name 01:14:49 MissPiggy: is conor mcbride on irc? 01:16:14 SheTyTyTy 01:16:16 shitty titty 01:19:12 alise no 01:19:44 which is good because he'd probably not get much done if he was 01:19:46 heh 01:19:53 okay, I've decided that it's totally fruitless using haskell for this 01:19:58 agda time???? 01:20:03 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:41 what error? 01:22:59 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:02 *strange. 01:23:31 the solution is to stop pretending to be a girl 01:23:44 who said i'm doing that now eh 01:23:51 PERHAPS MY MOTIVATION CHANGED, perhaps i just like this name 01:23:55 also stop pretending to be Canadian 01:24:22 oooooooooooooo 01:24:35 ?? 01:24:42 oh 01:24:42 eh 01:24:43 har har 01:25:06 http://en.wikipedia.org/wiki/Alice_(programming_language) ok, alise would not be a good name for the language 01:25:07 i don't get it 01:25:19 oklopol: canadians say eh, eh 01:25:24 -!- cheater2 has quit (Ping timeout: 276 seconds). 01:25:28 oh. 01:25:39 MissPiggy: what error did you get? 01:25:53 cabal: cannot configure QuickCheck-2.1.0.3. It requires ghc -any 01:25:53 There is no available version of ghc that satisfies -any 01:26:48 pigworker = conor right? 01:26:52 yeah 01:26:57 MissPiggy: just checking. you have ghc right :D 01:27:02 yes I have ghc lol 01:27:15 ehh, ask #haskell 01:29:42 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:29:43 asdfghjkl; 01:31:32 huh 01:31:36 that's odd 01:33:00 maybe i'll upgrade cabal-install 01:33:42 * Sgeo needs an ST monad tutorial 01:33:50 it's like io but only has iorefs 01:33:51 fin 01:34:00 Or something along the lines of how to hold onto state in Haskell 01:34:23 dude ST is awesome 01:34:38 what do you mean hold onto State though? 01:34:40 ST is about mutation 01:34:47 mutable reference with O(1) update 01:34:57 so might be the wrong thing 01:36:35 Sgeo: ST is for temporarily using (real) mutable state inside a theoretically pure computation 01:37:59 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:17 iirc 01:38:41 and if you just want to _simulate_ state using pure computations, use State / StateT 01:39:22 I want a nice tutorial on all of these 01:39:28 hm 01:39:44 haskell is learned by word-of-IRC 01:40:25 indeed, never seen a tutorial in my life 01:42:14 -!- alise has joined. 01:42:37 Tutorials are just lies that the MAN uses to keep us down. 01:42:48 yeah! 01:42:51 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:43:51 Antecedent 01:44:13 huh? 01:46:17 * Sgeo bookmarks 01:47:12 * coppro <3 LaTeX 01:57:17 MissPiggy: instead of a partial monad, would it be possible to have just an "infinite computation" monad? 01:57:25 dunno 01:57:26 just a thought 01:57:47 what's the difference 01:57:52 same thing no? 01:58:20 well, partial lets you have things in-between 01:58:24 few-steps-delayed 01:59:03 data Inf a = Further a (Inf a); bottom = Further bottom bottom -- I think 01:59:13 MissPiggy! 01:59:47 an infinite computation monad is just a partial monad where you cannot distinguish Further . Further from Further 01:59:52 i think 02:00:06 oerjan: it's a partial monad where Later has some not-fully-computed value, and there is no Now 02:00:24 oh right no Now either 02:00:27 hey augur :) 02:00:56 it's essentially opaque outside of runtime, then, like IO... 02:00:59 have you clarified your sex and/or gender to ehird? 02:01:13 clarified butter 02:01:18 melted and seived 02:01:34 i'd clarify your butter 02:01:38 lol 02:01:40 until you clarify we shall have to refer to you by the generic pronoun (s)h/it 02:01:57 :D 02:02:11 oerjan: not opaque 02:02:18 with a definition of the naturals you'd get 02:02:29 Further [] $ Further [1] $ Further [1,2] $ Futher [1,2,3] etc 02:02:37 Bottom would be Further ? $ Further ? $ Further ? 02:02:39 for some ? 02:03:03 Length of an infinite list would be Further 0 $ Further 1 $ Further 2 $ ... 02:03:09 argh the question mark, my old nemesis 02:03:19 aka fake unicode 02:03:26 It's an actual question mark. 02:03:34 i know, i checked the logs 02:03:37 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 With IO, for instance, you'd have an EndProgram event, and then just Nop, Nop, Nop forever, 02:03:51 *forever. 02:03:55 (they'd never be looked at) 02:04:07 i.e. main_ = main >> exitSuccess 02:04:10 erm 02:04:16 main_ = main >> exitSuccess >> main_ 02:05:49 as alise I am getting speedier help in #haskell! 02:06:55 alise: hm this is possibly isomorphic to Reader Natural 02:07:21 right but not in a total language 02:07:41 MissPiggy: btw does agda allow something like foo :: Void -> a; foo _ = bottom? 02:07:47 yes 02:07:49 if you have a Void you have bottom anyway, so you're not making anything worse 02:08:11 you can do 02:08:13 foo :: Void 02:08:15 foo = foo 02:08:19 if you turn off the termination checker 02:09:15 data Void where bottom :: Void -> a 02:09:31 oh wait 02:09:32 no, data Void 02:10:05 foo :: Void -> a 02:10:07 foo () 02:10:13 alise: foo x = case x of { } 02:10:24 that's the syntax to define it by "pattern match" on an empty type 02:11:07 that's intuitively correct, at least 02:11:38 MissPiggy: um you mean that foo () means the same thing? 02:11:46 Fun with the list monad: (| return ({[1..2]}, {[3..4]}) |) 02:11:53 oerjan same as what? 02:12:01 MissPiggy: as my case 02:12:18 oerjan, yeah (except that agda doesn't have case) 02:12:23 ok 02:12:32 oh wait this isn't agda is it? 02:12:36 oh it is.. 02:12:37 -!- Asztal has quit (Ping timeout: 265 seconds). 02:16:11 hmm... (| f {x} |) -> f <$> x, (| f {x} y |) -> join (f <$> x <*> return y) 02:18:01 (| 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 oh, and (| x; y |) -> do (| x |); (| y |) 02:23:33 cat = (| putStr {getContents} |) 02:23:50 catLines = (| putStrLn {getLine}; catLines |) 02:24:19 MissPiggy: I wonder if you could make that table thing into the actual data type system of a functional lang 02:24:34 a gadt is shorthand for creating a table and adding some rows 02:24:43 functions are automatically turned into columns 02:25:04 (if they pattern match on the constructors; otherwise, they must be compositions of existing functions that do) 02:25:10 (and so don't need to be columns) 02:25:27 add some syntax for adding rows and voila 02:27:02 -!- SimonRC has joined. 02:27:04 yeah it could work 02:27:06 I think! 02:27:20 but well it only defines a small class of functions 02:27:26 (one that are folds) 02:27:35 I don't see what you mean 02:28:01 also, it's ridiculous how much low hanging fruit there is in abstraction design 02:28:21 dependent types. a powerful module system ala ML. these tables. etc. 02:28:31 Yet nobody is putting them into their languages. 02:29:13 about time to start doing it I think :) 02:29:23 i'm on it 02:29:56 i'm so gonna have to hire some phds to write the compiler, though 02:30:18 proving the type system sound with all this stuff will be *way* out of my league for one :P 02:31:07 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 then you don't have to worry about consistency 02:31:32 this is the approach Coq takes (And the one Agda doesn't) 02:31:39 well, that's my plan, but some of the features would be really, really convoluted to compile 02:31:43 so need to be in the base language 02:31:46 and thus complicate things 02:31:53 ah I see what you mean 02:31:58 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:32:51 literal brackets 02:33:01 a pair of brackets whose contents is interpreted according to a separate, extensible syntax 02:33:03 why? 02:33:29 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 template haskell comes close to that, but not quite 02:35:45 (in one of its features) 02:36:44 (| email {fileContents <~/message.txt>} |) 02:42:11 It'd be nice if there was a way to do symbolic computation without writing a parser in the lang 02:43:28 just have a Symbolic type 02:43:34 and use expression templates 02:43:52 whatever that is, it's probably a C++ abomination. 02:44:28 Expression templates are when overloading is used to build up expressions in data 02:44:57 e.g. x^2 might give some value which represents "x^2", which is exactly what you want in symbolic computation. 02:45:02 It's more the "any undefined value just sits there" thing. 02:45:46 what about transcendental constants? For accurate math, they must be treated very much like unknowns 02:48:11 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 Time for GREGOR'S LANGUAGE CHALLENGE 03:00:07 Write a language with the following name: 03:00:11 ATTACK OF THE FLYING MONADS 03:01:10 alise: That seems like a pretty easy feature to add 03:03:56 Adding arbitrary features is bad. Adding general constructs is good./ 03:03:57 *good. 03:14:39 MissPiggy: would you believe i'm still at the "install agda" step in my dependent lc plan... >_< 03:14:40 i hate software 03:14:53 me too it sucks 03:15:19 and _this_ is why i have a grand os vision >:| 03:16:30 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:00 it's called Debian 03:18:26 yeah everything's called something else if you ignore pertinent words like decentralised, type signatures, and value ecosystem 03:18:49 Debian supports decentralisation 03:19:03 if you believe your statement, you are not using the word i meant. 03:19:07 don't even know what you mean by type signatures and value ecosystem 03:19:35 then perhaps you shouldn't make snarky comments about debian 03:19:44 no, I just assume you're insane 03:19:51 :P 03:19:57 actually, you know what? I retract that 03:19:58 it wasn't funny 03:20:10 bitbucket :: a -> () 03:20:13 bitbucket _ = () 03:20:15 > bitbucket coppro 03:20:35 coppro: perhaps slightly inappropriate given my current situation :P 03:20:43 retraction accepted, but i don't really mind 03:20:47 wait, we cannot claim we're all mad here any more? damn doctors. 03:20:59 alise: "value ecosystem" turns up 0 relevant hits 03:21:13 so does your face. 03:21:21 as for type signatures, I have no clue how that relates to packages 03:22:05 if you understood "value ecosystem" it would make more sense :P 03:22:25 then explain it, because apparently you're the only one who does 03:23:00 Gregor: Attack of the Flying Monads, eh? 03:23:03 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 like that, but with functional-programming values instead of objects. 03:23:18 ah 03:23:21 pikhq: No, ATTACK OF THE FLYING MONADS 03:23:27 Gregor: Definitely needs to use the function instance for monads as the only way to be Turing-complete. 03:23:36 alise: I retract my retraction :P 03:23:39 That (except for the functional bits) sounds like Unununium 03:23:48 (>>= is S, return is K) 03:23:49 coppro: yeah my system isn't unusable, i must be crazy 03:24:03 (... Erm, no. >>= is not S. XD.) 03:24:08 Grog XD. 03:24:16 S is ap 03:24:22 Sgeo: Roentgenium 03:24:24 Yes. 03:24:39 And ap is defined in terms of return and >>=... 03:24:50 hm lessee 03:24:58 So, >>= and return suffice for combinator calculus. 03:25:00 alise: It's a pipe dream. 03:25:06 coppro: the os is called unununium 03:25:09 also, it's very much not 03:25:17 these techniques are actually simpler to implement than a traditional unix system 03:25:19 (f >>= g) x = g (f x) x 03:25:24 it's not one additional layer, it's one _less_ layer of separation 03:25:29 Yes, I know. 03:25:43 I just had a bit of a thinko. 03:25:49 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 But it's one layer trying to abstract toom uch 03:25:56 *too much 03:25:59 you are wrong, and do not understand it 03:26:04 occasionally pipe dreams work out 03:26:07 for one, smalltalk has existed since the 70s, and its implementation was _very_ simple 03:26:10 for two, run Squeak right now 03:26:13 sure 03:26:15 you're using the exact thing I'm describing 03:26:22 but as an OS? 03:26:23 for three, see Oberon OS. it fits on a floppy and does just this. 03:26:26 Squeak is an OS in a box 03:26:27 smalltalk is an os 03:26:29 it was an os 03:26:31 it booted up the computer 03:26:34 squeak is descended from it 03:26:38 it's just in a window now 03:26:42 Smalltalk is one of the simpler OSes. 03:27:05 Since all that the "OS" is is a language runtime... 03:27:11 * Sgeo searches for Smalltalk.NET 03:27:16 ah, I think I am misunderstanding 03:27:19 Everything else is just your library. 03:27:27 coppro: How did you interpret it? 03:28:09 eh, I'm not really sure 03:28:18 * coppro tries to think it through 03:29:03 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 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 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 And... well, that's it. 03:29:53 * coppro needs sleep, he thinks 03:30:02 The computer's memory becomes a disk cache, and the disk is full of values. 03:30:05 With types. 03:31:01 okay, pretend I wasn't a part of this conversation. I think I was insane. 03:31:08 A lot of insanity. 03:31:13 what were you thinking? :P 03:31:33 oerjan: Just discussing ideas for ATTACK OF THE FLYING MONADS. 03:31:41 oerjan: Don't necessarily need Haskell's type system. 03:31:51 alise: I'm not sure what I was thinking. Which is why I think I was insane. 03:32:25 pikhq: note that it says MONAD_S_. you cannot use just one ;D 03:32:36 oerjan: Yes, I know. 03:32:49 oerjan: I'm just saying the function instance should be the only thing making it TC. :P 03:33:25 there's no reason we have to use the programming concept 03:33:29 hm maybe that reverse state monad would be something for getting fix-points... 03:33:59 then it can still be well-typed 03:34:13 i <3 the reverse state monad 03:34:38 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:37:22 bach did that? 03:37:28 err 03:37:30 Beethoven 03:37:32 * coppro whistles 03:37:44 Bachovenzart 03:38:53 that would require some reverse state indeed, bach died before schiller was born (1750 vs. 1759) 03:40:42 hm a language based on time travelling anachronisms... 03:41:23 to quit the program, you need to get hitler eaten by a dinosaur. 03:41:50 without causing an alternate world war to take its pace 03:41:51 *place 03:42:16 _may be_ 03:42:22 yes! 03:42:24 wikihistory esolang 03:42:47 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:42:51 is anyone here on vista? 03:42:54 :x 03:42:59 or win 7? 03:43:08 No, but I do have erectile dysfunction. 03:43:09 * Sgeo is on WinXP 03:43:14 We all have our issues. 03:45:10 Me: My email address is ********@gmail.com 03:45:16 Other person: thats yahoo? 03:45:51 alise: you're pulling off the female thing really badly 03:46:51 Sgeo: Just send the $500,000 so we can complete the transaction. 03:46:56 coppro: i know rite 03:47:04 coppro: well everyone knows i'm male in here so there's hardly any point 03:47:08 and the only other place i dwell is #haskell! 03:47:09 true 03:47:13 but that's your own fault! 03:47:19 Talking to someone who randomly came to a nearly dead chat 03:47:27 so the only affect of this is that i'm referring to myself as "she". well, when i remember. 03:47:46 alise: no wait, erectile dysfunction means you cannot be male, right 03:48:04 * alise scratches head 03:48:05 o.O 03:48:10 The person invited me to private chat 03:48:19 I was in another tab, but I accepted 03:48:19 SEXY TIME 03:48:24 THat meant I couldn't see the main chat 03:48:53 Just closed out of private chat... and apparently before I went into private chat, e said "Let's have sex" 03:49:19 Ha! I was RIGHT! 03:51:43 sex chat... usually that's hard because there's not many girls on IRC 03:52:02 it was probably in one of sgeo's endless obsessions^Wshitty 3d virtual-reality games from years ago. 03:52:13 alise, you're psychic 03:52:40 actually the universe has shown a disturbing tendency to shape what i experience according to me recently 03:53:54 madbr: Though, if you're gay you shouldn't have *too* much trouble. 03:54:21 At least insofar as I can tell, there's more gay men than there are females on IRC. (in general) 03:54:21 Or botsexual. 03:54:37 If you're botsexual, then it's trivial. 03:55:06 pikhq: yes 03:55:16 Or silensexual. 03:55:26 /ignore *@* 03:55:49 coppro: i'm not ready for that kind of commitment. 03:55:56 :P 03:56:01 coppro: /join #brainfuck 03:56:15 why? 03:56:26 Silent. 03:56:36 ah 03:58:30 Sex chat is easy so long as you're not so damn picky :P 03:59:08 He knows this from extensive ... research,. 03:59:10 *research. 03:59:39 -!- Sgeo has quit (Ping timeout: 256 seconds). 03:59:57 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 Clearly, everyone should only have sex chat with Egobot. 04:00:20 `echo I put on my robe and wizard's hat. 04:00:21 I put on my robe and wizard's hat. 04:00:23 Gregor: THE IRC SERVER INBETWEEN 04:00:26 It knows everything 04:00:27 EVERYTHING 04:00:29 OH GOD THE HORROR 04:00:49 ah, it has probably seen much worse 04:01:20 "I fling my dung-covered vomit into your urethra." 04:01:28 HOT 04:01:44 Urinal tract infections are SO SEXY. 04:02:46 urinalot of trouble 04:04:54 seen worse 04:06:19 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:52 I have a fetish... 04:07:53 for LOVE 04:07:55 -!- alise has quit (Ping timeout: 248 seconds). 04:07:58 -!- alise_ has changed nick to alise. 04:08:03 'tis a good thing 04:08:11 -!- Sgeo has joined. 04:08:44 That was screwed ip 04:09:00 ip ip ip 04:09:06 SCREWED, ey? 04:09:35 look, I already told you to stop being Canadian. Switching to a y doesn't count. 04:10:58 uhh 04:11:00 maple syrup 04:11:00 eh 04:11:01 eh 04:11:02 eh 04:11:02 eh 04:11:03 eh 04:11:03 eh 04:11:03 eh 04:11:04 eh 04:11:04 eh 04:11:04 eh 04:11:09 ^ canadians 04:11:37 There's no canada like french canada 04:12:52 maple syrup is indeed delicious 04:13:21 So is chapstick >.> 04:14:21 I'm beginning to suspect that chapstick is an euphemism for something else 04:14:38 I'm going to assume it isn't 04:14:43 everything in english is an euphemism for sex 04:16:16 i'm afreud so 04:16:26 madbr: including "english"? 04:16:34 Or how about ... discombobulated 04:16:43 I'll give you english lessons 04:16:48 ooh, look at those bobules 04:17:03 madbr: No, just everything written by Shakespeare. 04:18:02 Country matters. 04:18:49 http://tvtropes.org/pmwiki/pmwiki.php/Main/CountryMatters 04:19:47 I love that Ulysses quote. 04:22:07 sgeo: heh, eventually we'll wear out "fuck" and have to switch to "cunt 04:22:08 " 04:27:44 g 04:27:59 i keep reading my name as aisle 04:28:17 Pick up the phone booth and aisle? 04:28:44 actually that might be a plan if you're a rapper that sells disks to 11 year olds by saying obscenities 04:47:19 amasses of obulence 04:49:29 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 Chapstick, folks. Chapstick. 04:51:06 My chapstick is tingling. 04:55:09 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:27 HM 06:39:41 Most examples of using this particular SDK are C. This example is C++ 06:40:06 Wait, no 06:40:08 Wait, yes 06:41:23 O_o 06:41:27 link? 06:41:34 http://wiki.activeworlds.com/index.php?title=Aw_laser_beam 06:42:40 which is C++? 06:42:43 oh 06:42:45 yeah, I see 06:42:46 hah 06:43:37 At first, I forgot that C had structs, so I thought the whole Line thing wouldn't make sense 06:43:56 Then I realized it does.. but it doesn't have the & pass-by-reference thing.. I think 06:44:38 yeah 06:44:41 Only pointers. 06:45:14 The & stuff is somewhat confusing, tbh 06:45:32 I don't know why people think pointers are complicated. IMO, they make more sense 06:47:32 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 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). 09:54:37 sup guys 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 To converse at the distance of the Indes by means of sympathetic contrivances 11:10:53 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 [07:32] 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 coppro: remember what I said about me seeming to shape the universe? 14:08:56 it's getting ridiculous lately. 14:09:30 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 oerjan: whatever curse you've put on me, stop it 14:20:58 wait, what? i was trying to put a curse on your doctors, not you. must have missed slightly. 14:23:37 also i was pondering more scientific plans. unfortunately they all involve first inventing a working teleport device. 14:28:13 the universe has been freaking me out since before that :p 14:28:48 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 yes, but there's simply not enough space in the non-synchronicitious day for other people to have all theirs, too 14:30:36 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 wait, you are affecting the TV news? 14:31:49 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 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 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 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 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 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 from a 1-second google it's actually postulating that luck exists and some have it more than others? 14:45:08 so much for "scientific" 14:45:14 (well it's more in a popular science form) 14:45:32 "In this book Richard Wiseman, former magician turned" 14:45:42 james randi is the only one who can pull off that :P 14:46:54 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 i.e. even _if_ it's all about perception, you can still affect your luck by changing it. 14:48:04 Only through working harder to do better (in ways that minutely change seemingly "random" outcomes) because you think you will... 14:48:24 Which isn't really changing your luck at all, luck would be affecting things you have no control over. 14:49:11 perhaps. this book is about the part you can control though, and why it's still important. 14:49:47 Well, I don't call things like that chance. 14:50:35 _i_ think there's more than that, of course. 14:51:03 but that book imho goes as far as you can _without_ leaving the scientific worldview 14:51:06 Many mathematicians seem to believe in the orbiting teapots, though I can't fathom why them specifically. 14:51:14 it was sort of gateway drug for me really 14:51:21 Maybe because their rational system doesn't say anything about the world. 14:51:28 So they don't make the connection... 14:52:58 whatever. i'll just have to wait for you to change your opinion ;D 14:55:39 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 Although I'm a lazy slob and don't tend to follow my utilitarian aspirations. 14:56:56 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 You believe in something entirely unfalsifiable. 14:57:22 That is irrational by definition. 14:57:40 * oerjan sets fire to alise's strawman 14:57:55 Then what do you believe? 14:58:37 godchat 14:59:10 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 Define synchronicities. 14:59:47 how do you spot a time when it's important to happen 14:59:56 Pthing: because it happened, obviously! :P 14:59:57 i guess _you_ have never been followed home by a three-legged black kitten when in a particularly self-destructive mood. 15:00:08 a kitten deciding to follow you 15:00:15 and it lost a leg because of some happening? 15:00:21 man, that's spoooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooooky 15:01:26 whatever. 15:01:33 i mean it 15:01:36 how do you tell 15:01:52 surely there are instances where it could be really important one happens but it doesn't 15:01:52 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:03 yes, yes. 15:02:10 ok so i'm not rational. 15:02:42 That sure was easier to convince you of thaan it is for most. Are you sure you didn't already believe that? 15:02:46 *than 15:02:58 heh 15:03:01 jesus christ, you weren't convincing 15:03:14 i am not _intending_ to be convincing. 15:03:20 i meant alise 15:03:43 a second ago he was claiming he was rational. 15:03:49 anyway i didn't say i was convincing 15:03:53 that was not the word i used 15:04:06 "convince" is the word 15:07:35 ok i'm uncomfortable continuing this conversation. if it's because i'm irrational, so be it. 15:08:13 now iwc. 15:11:30 don't worry martians, the froghurt is cursed anyhow 15:13:42 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 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 hm played with ghostscript's image backends 15:30:16 they give ugly results 15:30:21 non-antialiased 15:33:09 -!- MissPiggy has joined. 15:33:22 hi MissPiggy! 15:34:07 hey 15:34:16 what's happening 15:34:24 stuffs 15:38:17 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 and that gives antialiased output 15:44:16 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 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 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 Ilari: Well, it's relative to the type (∃a.a). 15:46:30 alise that sonuds insane 15:46:38 can you even compute that? 15:47:01 MissPiggy: well for the typechecker it's easy 15:47:12 if the value is in the set we complemented, go all beepy like 15:47:14 otherwise, smile 15:47:27 you could construct a type of "everything you cannot `show` (as in Haskell show)" :D 15:47:40 hah 15:47:58 * Sgeo is learning the joy of watching TED talks 15:47:59 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 MissPiggy: i guess it's more useful to have complements 15:49:07 then you can just do (∃a.a) - foo 15:49:10 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 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 hmm, what uber-general concept can we apply to - to let us define it on sets? :-) 15:49:24 sounds a bit SET THEORY to me 15:49:27 hmm... maybe sets are haskell-ish Nums 15:49:27 * MissPiggy pitchforks 15:49:34 (+) :: Set -> Set -> Set, yes 15:49:49 Hm 15:49:52 (-) :: Set -> Set -> Set, yar 15:50:03 In my Data Structures class, we made a fraction calculator in C++ 15:50:05 (*) :: Set -> Set -> Set, that'd be a tuple 15:50:12 Maybe I should make a similar calculator in Haskell 15:50:25 MissPiggy: Quick, what's set `div` set?! 15:50:27 :P 15:50:34 (Not required for Num, but amusing to think about anyway.) 15:51:18 One property of sets is that for any set, there is strictly larger set. 15:53:03 More construcively: All sets have powerset, and that powerset is always strictly larger than the set itself. 15:53:48 There's no bigger set than (∃a.a). 15:53:50 is that a property of sets hm 15:53:57 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:39 it's exists :P 15:54:44 Sgeo: It's flipped E. 15:54:46 (exists) 15:54:52 alise: If there isn't anything bigger than it, it can't be a set, it is proper class. 15:54:54 oh 15:55:07 In haskell, you would write it (forall a. a) because it overloads forall for existential quantification. 15:55:17 Ilari: Yes, but type theorists poop on set theory for breakfast. 15:57:09 Another funky feature: Sets with cardinality above Aleph-0 include undescribable elements. 15:57:57 Such is the strange world of the Curry-Howard isomorphism. 15:59:22 Hmm. 15:59:44 -!- kar8nga has joined. 15:59:47 (\(x::T). ...) -> (\x. (\x'. ...) (x::T)) if you have ::. 16:00:17 -!- Asztal has joined. 16:00:48 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 *Main> L (TyTy :-> (\(T a) -> a :-> (\_ -> a))) :1:0: No instance for (Show (ID -> Term -> Term)) 16:05:53 Woot 16:06:16 (That's (\...) :: (a::Set) -> a -> a) 16:08:14 Hmm. 16:08:19 I don't actually need to have separate Term and Set types. 16:08:49 L :: Term -> (Term -> Term) -> Term 16:08:51 (:->) :: Term -> (Term -> Term) -> Term 16:09:01 Whenever I see two things of the same type, I feel this intense urge to unify them. 16:09:11 But they're not the same :p 16:09:12 *:P 16:10:26 Starting to think that that function idea isn't so great, though, because then I can't, you know, show lambdas. 16:12:48 idL = L (A SetSet (A (N Top) (N (Dip Top)))) (N Top) 16:12:49 That's better. 16:14:56 * Sgeo drinks a Red Bull shot 16:15:02 * alise drinks a horse 16:15:18 It came free with a few hundred dollars worth of books 16:15:42 Let me guess, it's awful and terrible for you. 16:15:55 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 Don't let Ilari hear about this or you'll never stop hearing about sugar :-) 16:16:07 *coffee, also. 16:16:52 He says if I want something convenient, there are pills 16:17:33 Or how about sleeping better and not needing things like that. 16:17:36 *Main> idL \((*) -> (t) -> dt). t 16:17:37 Woot 16:19:05 If sugar's main issue is that it causes obesity or something, I don't see a problem 16:19:29 Destroys your liver 16:19:49 Oh 16:21:20 -!- jcp has joined. 16:26:37 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 And I hate the taste of coffee 16:29:38 Drink tea. It has more caffeine. 16:30:14 Drinking tea takes time 16:31:16 MissPiggy: HALP http://pastie.org/813531.txt?key=ahcwvmgdprki24beyw5gq 16:31:24 Sgeo: So does coffee 16:31:35 alise, indeed 16:31:45 Anyway if you want a cheap boost the expense of your health feel free. 16:31:46 whatos :.? 16:31:50 Drinking this Red Bull shot took maybe a few seconds 16:31:50 , he said, while drinking cola. 16:31:55 MissPiggy: application 16:32:03 I would call it :$ but it's left-associative As God Intended 16:32:23 rT is 16:32:23 uh 16:32:24 in 16:32:27 (x::T) -> ... 16:32:32 rT is the ... 16:32:38 f : (a : A) -> B[a], 16:32:43 x : a |- 16:32:45 wait, rT isn't actually a function 16:32:46 f x : B[x] 16:32:52 so i can't do that 16:33:00 L :: Term -> Term -> Term A :: Term -> Term -> Term 16:33:08 maybe the second Term _should_ be a lambda 16:33:13 so that it's expressed as T -> (\x -> ...) 16:33:19 yeah you could try that 16:33:24 is that haskell though? 16:33:36 yeah but it'd actually be written as 16:33:38 not with a real lambda 16:33:40 but with an L term 16:33:41 you can't do HOAS in agda 16:33:44 oh oky 16:33:55 like 16:33:59 idL = L (A SetSet (A (N Top) (N (Dip Top)))) (N Top) 16:34:03 (N is the variable stuff) 16:34:18 A, arrow, pushes a new variable and runs the code 16:34:26 so does L, so maybe A's second argument should be an L 16:37:14 In fact, I think I meant it to be an L. 16:37:39 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:39:32 hmm 16:40:31 i was thinking i could rely on glorious laziness to bottom out in the end but i don't think so 16:41:22 for a well typed program you don't need to worry about evaluation order 16:42:37 yeah but my typechecker is sequential not lazy 16:42:40 maybe monad 16:43:05 the problem is that every type is, I think, infinite 16:43:11 every type has a type of the type and the typey type type 16:45:39 infinite O_O 16:45:46 well you can just stop at Set 16:45:48 INFINITE DIMENSIONS OF THE COSMIC SOUL 16:45:50 Set is well formed 16:45:54 yeah but 16:45:57 ok lemme give you an example 16:46:40 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 (\(* -> t -> dt) -> t) whatever 16:46:54 erm 16:46:57 right 16:46:57 so 16:47:05 first we get the function's type 16:47:07 simple enough 16:47:12 then whatever's typef 16:47:14 *type 16:47:21 then we check the types match 16:47:22 but now 16:47:27 we have to pass whatever to the (t -> dt) bit 16:47:36 which is a function, it needs to be typeofwhatever -> set 16:47:41 so we need to check it 16:47:45 check (that bit :. whatever) 16:47:50 ...but we're in the clause for (f :. x) 16:47:52 so we go forever 16:47:54 get it? 16:48:00 no 16:48:25 why not 16:48:35 oh wait 16:48:39 A's argument can't be an L 16:48:45 because that would cause an infinite nestingness 16:48:45 okay 16:48:48 i may be able to solve this with my genius 16:48:52 i'm terribly clever 16:48:55 lol 16:49:09 heh, to write my typechecker i need to write eval :/ 16:49:25 yes you do 16:49:31 yep. 16:49:36 that's expectet 16:49:44 yeah, still :P 16:49:45 fuck, at the end of this I'm going to write Term -> String 16:49:48 its name? 16:49:49 by the way 16:49:49 toC 16:49:58 if there's one thing i'm getting out of this hellhole of coding 16:49:58 eval is pretty easy to write 16:50:03 i'm gonna get some half-efficient code 16:50:05 yeah i know 16:50:13 http://sneezy.cs.nott.ac.uk/fplunch/weblog/?p=95 16:50:16 this technique 16:50:17 using `data ID = Top | Dip ID` for my names will make renaming and shit really terribly easy 16:50:18 NbE 16:50:39 well, that type is just de bruijn 16:50:43 it's just nat 16:50:47 maybe i should just use ints 16:50:53 MissPiggy: i can't use that technique, can't use haskell funcs 16:50:57 want to be able to `show` things nicely 16:50:58 why not? 16:51:08 you can quote it and show the quoted form 16:51:14 ro you could implement show on the functions 16:51:17 ? 16:51:21 just apply them to a gensym 16:51:25 hmm 16:51:26 good idea, maybe 16:51:31 yeah ok 16:51:38 so wait. 16:51:44 why do i need de bruijn stuff 16:51:47 if i have it as functions 16:52:06 or the syntax :P 16:52:13 ? 16:52:29 i'm confused 16:52:50 well the syntax should be de bruijn, and the semantics is haskell functions 16:53:11 hmmm, does it even need to be de bruijn 16:53:18 maybe you are right and it doesn't matter 16:53:36 i'm not sure anymore 16:54:00 well 16:54:04 I need some sort of name to do the "pass the gensym" 16:54:21 so i guess it's best to keep it like that 16:54:43 you know what, I'm gonna write my evaluator first 16:54:45 then my typechecker 16:58:16 -!- MigoMipo has quit (Remote host closed the connection). 16:59:58 MissPiggy: that post confuses me 17:00:05 why does it have a separate type for evaluation? 17:00:58 let me explain a simpler version 17:01:23 suppose you have a syntax like: data Exp = Num Int | Var Ref | Add Exp Exp, 17:01:43 ya 17:01:51 hmmmmmm that was a bad example 17:01:57 no variable binding :P 17:02:33 well the point is this, you have a type Syntax and another type Semantics, 17:02:44 eval :: Syntax -> Semantics, quote :: Semantics -> Syntax 17:02:51 now normalize = quote . eval :: Syntax -> Syntax, 17:03:20 the reason it gives you a normal form is because factoring through Semantics quotients out anything you don't care about 17:03:34 tell you what i'll just do it how the article says 17:03:45 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 but as far as i can tell Syntax = Semantics if I use haskell functions in the actual data types 17:04:08 then normalize ((p * q) * x * (y * z)) = p * (q * (x * (y * z))) 17:04:30 now if we use the semantic domain Sem = Sem -> Sem, we have a model of lambda calculus 17:04:41 and thats why it does beta normalization 17:05:22 (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 if you use HOAS, syntax might be: data Syn = F (Syn -> Syn) | App Syn Syn | ..., 17:05:59 Sem doesn't have App 17:07:12 ok, so Sem is the untyped lambdas 17:07:19 and Syn is my dependently-typed language in its entirety 17:07:31 why Var Ref 17:07:36 why not just keep track of vars with haskell arguments 17:07:55 well you could I dunno 17:08:19 the reason that I like ints for bound variables is you can do eval context (Var ref) = context ! ref 17:08:34 oh that should be !! 17:09:20 what i mean is 17:09:23 you don't need variable bindings 17:09:25 because Sem -> Sem 17:09:27 the first Sem gets a name 17:09:28 voila 17:11:26 no? 17:19:57 MissPiggy: :/ 17:20:00 this is confusing 17:20:57 eyeah it 17:20:58 is 17:21:03 I'll help 17:21:46 yaay<3 17:25:41 look at this trivial example 17:25:53 data Syn = N Int | Add Syn Syn 17:25:57 data Sem = Sem Int 17:26:16 eval (N i) = Sem i ; eval (Add x y) = eval x <+> eval y 17:26:21 quote (Sem i) = N i 17:26:51 yah 17:26:59 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:18 x === y --> nf x == nf y 17:27:27 === is extensional equality, and == is syntactic 17:27:57 so you can also do something like monoid simplification, 17:28:16 data Syn = Id | Var V | Op Syn Syn 17:28:26 data Sem = Sem [V] 17:28:37 ok, can i tell you the "issue" i'm having in code? 17:28:42 eval (Id) = [] ; eval (Var v) = [v] ; eval (Op x y) = eval x ++ eval y 17:28:47 oops 17:28:51 should be <++> 17:29:08 data Syn = Lam (Syn -> Syn) | App Syn Syn 17:29:13 quote (Sem []) = Id ; quote (Sem (x:xs)) = Op x (quote (Sem xs)) 17:29:16 one, what's the Sem for this? and two, when I quote it, how would I stringify it? 17:29:21 there's no "dummy gensyms" to pass 17:29:34 and you have nf = quote . eval, and nf normalizes out identity and associativity 17:29:37 !!!!!!!!!! 17:30:08 yes Syn is a bit harder, we can build it up in two stages 17:30:24 data Sem = Sem (Sem -> Sem) 17:30:38 eval (Lam f) = Sem (\x -> eval (f x)) 17:30:47 eval (App f x) = eval f <$> eval x 17:30:59 Sem f <$> x = f x 17:31:07 now of course you can't quote this yet, 17:31:35 so we can add 17:31:42 data Sem = ... | Neutral N 17:31:56 data N = NVar Var | NApp N Sem 17:32:04 * Sgeo looks at some old Haskell code he wrote to try to get a taste for Haskell again 17:32:19 MissPiggy: that confuses me 17:32:59 I can't believe I actually wrote 17:32:59 What exactly happened here is that we generalized the problem - in order to make recursion work on it 17:32:59 show $ uncurry quad $ (\(x:y:[]) -> (x,y)) $ map read $ words line 17:33:06 * Sgeo should attempt to understand that 17:33:17 this is pretty much always a magic step, but it'll becme obvious in retrospect 17:33:19 MissPiggy: I'll have to think about this 17:33:24 maybe I should write the typechecker first :P 17:33:27 (same with induction proofs, when you do a magic generalization) 17:33:36 typechecker is Syn -> Maybe Syn (Syn includes types), not Sem right? 17:33:41 even though it involves evaluation at some point 17:33:45 anyway, the idea is that we generalized from CLOSED terms, to OPEN terms with N free vars, 17:33:49 clearly CLOSE = OPEN 0 17:33:57 but now we have OPEN n (any n) 17:34:03 i must be really dumb today :) 17:34:38 so if we have an term like OPEN 3, suppose the context is [oa, ob, oc] 17:34:39 Ok, I understand what it does now :D 17:34:47 I don't know if I could ever write it again though 17:34:53 Plus, there's probably a more elegant way 17:35:02 and the term is maybe Sem (\x -> oa <$> x <$> ob) 17:35:54 well 17:36:42 the term is Sem (\x -> Neutral (NVar oa) <$> x <$> Neutral (NVar ob)) 17:36:42 anyway, 17:36:42 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 of course you substitute x into say Neutral (NVar od) 17:37:29 once the lambda body is quoted you abstract it back out to get a syntax lambda term 17:38:25 ^ this is one bit where de bruijn syntax is slightly easier/nicer than HOAS I guess 17:41:13 You can also make quote type directed, so that it eta-expands 17:41:21 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 Kind of annoying how you have to read it from right to left. 17:44:19 Probably I should paste the whole thing 17:44:26 Well, what does quad do? 17:44:49 http://hpaste.org/fastcgi/hpaste.fcgi/view?id=17242 17:44:58 MissPiggy: isn't this more complicated than a syn->syn reductor :P 17:45:24 hm I don't know 17:46:01 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 I guess that looks pretty simple. 17:47:07 I think the semantic domain way has better theoretical properties 17:47:59 but if you don't need them... 17:48:20 `translate Suomen kieli eli suomi kuuluu uralilaiseen kielikuntaan ja sen suomalais-ugrilaisen haaran itämerensuomalaisiin kieliin. 17:48:23 The Finnish language, ie Finnish belongs to Uralic language family, and the Finno-Ugric branch of the Baltic-Finnish languages. 17:48:35 That's a very good automatic translation! 17:48:48 `translatefromto fi en eli 17:48:49 ie 17:49:02 I guess ie is an English word now. :) 17:49:28 Yeah, I think that translation is pretty much perfect. 17:49:56 `translate kielikuntaan 17:49:58 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 `translatefromto fi en kielikuntaan 17:50:13 language family 17:50:51 `translatefromto fi en haaran 17:50:53 branch 17:52:38 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 It would seem that my SKI interpreter, though much slower, does not have the severe memory leaks of the Lazy K interpreter. 17:52:55 thats's good!! 17:53:20 In lazyk.cpp, rot13 takes gobs of memory. 17:53:28 `translatefromto fi en kielikuntaankin 17:53:29 Language Board in 17:53:34 In my SKI interpreter, rot13 runs in constant space. 17:53:45 The power of garbage collection. 17:53:54 `translatefromto fi en haarankin 17:53:56 branch in 17:54:17 `translate haarankin 17:54:19 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:23 Sweet :P 17:54:59 `translateto he Oy, this has a lovely bunch of coconuts in it! 17:55:01 אוי, זו חבורה מקסימה של קוקוסים בו! 17:55:08 `translateto he in it 17:55:10 αδ 17:55:23 That looks like 'ad' in Greek. 17:55:44 :D 17:56:33 `translateto he in it in it in it in it in it 17:56:34 αδ αδ αδ αδ αδ 17:57:26 `translatefromto fi en puhujia 17:57:27 speakers 17:57:39 `translatefromto fi en miljoonaa 17:57:39 That was accurate 17:57:41 million 17:58:00 `translatefromto fi en on noin viisi miljoonaa 17:58:02 is around five million 17:59:14 `translatefromto fi en ei ole noin viittä miljoonaakaan 17:59:15 not even about five million 18:00:07 Does "Suomen kielen puhujia on noin viisi miljoonaa" literally mean "Finnish speakers are around five million"? 18:00:44 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 As a literal translation, something like that, yeah. 18:00:53 "There are around five million Finnish speakers" 18:01:22 But no, it's not like that 18:01:51 If you want the nonsense "Finnish speakers are around five million" literally translated: "Suomen kielen puhujat ovat noin viisi miljoonaa" 18:02:47 "Puhujia on" and "puhujat ovat" seem to be too many words for what they mean. 18:03:20 Not that I knew any Finnish at all before coming into this. 18:03:39 `translatefromto fi en puhujia on 18:03:41 "Puhujia on x" == "there are x speakers"; "puhujat ovat x" == "[the?] speakers are x" 18:03:41 speakers 18:03:53 That's not too helpful :-P 18:03:56 `translatefromto fi en puhujia 18:03:58 speakers 18:03:59 `translatefromto fi en puhujat 18:04:00 speakers 18:04:01 `translatefromto fi en puhujia on 18:04:03 speakers 18:04:03 Quite. 18:04:04 `translatefromto fi en puhujat ovat 18:04:05 speakers 18:04:09 `translatefromto fi en kaiuttimet 18:04:10 Speakers 18:04:13 heh 18:04:31 Are those the electric kind? 18:04:35 Yep 18:05:01 Anyway, yeah, I was forgetting that "puhuj-" is "speakers". 18:05:11 What's the citation form of that? 18:05:16 Citation form? 18:05:32 The form you would find in a dictionary. 18:05:54 You'd probably find the singular, "puhuja". 18:05:59 * uorygl nods. 18:06:01 I'm still not quite sure what you're after. 18:06:12 Probably that. 18:06:18 You might not even find that, you'd only find "to speak", "puhua". 18:06:29 I'm not sure how dictionaries deal with this kind of thing. 18:06:40 "Puhuja" is probably common enough by itself that you'd find it as well. 18:06:44 What case is "puhuja"? Nominative? 18:07:04 Yeah, nominative 18:07:10 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 See, you'd only find the first in a dictionary :-P 18:10:25 A verb equivalent, though the body text here is in Finnish as well: http://koti.mbnet.fi/henrihe/tiede/verbikaava.html 18:11:21 `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 "Why learning Haskell/Python makes you a worse programmer" 18:11:23 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 Sgeo: "Oh no it lets you write things more easily!" 18:11:47 Well, that translation doesn't really make sense. 18:12:08 pikhq, it seems to be more that you get spoiled 18:12:10 http://lukeplant.me.uk/blog/posts/why-learning-haskell-python-makes-you-a-worse-programmer/ 18:12:29 Seems fairly understandable to me 18:13:09 haskell-python? 18:13:12 is that the new C/C++? 18:13:20 "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 Doesn't make much sense to me. 18:13:51 You need to insert an "are" after "groups" 18:14:29 And the thing at the end is trying to say that they have disappeared over the 1900s 18:14:38 * uorygl nods. 18:14:48 Sgeo: So... 18:14:55 It's mostly the former issue that's confusing, IMO. 18:15:07 "Oh no it lets the computer focus on the trivial stuff" 18:16:15 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 `translatefromto fi en vanhoja 18:16:27 old 18:16:54 Sgeo: So, he sucks at programming, and languages aren't going to change that. 18:16:54 Got it. 18:16:57 Finnish->English is so non-injective :-) 18:20:13 It's so convenient how no matter what channel I'm in, there are always suomen puhujia close at hand. :P 18:23:07 Yeah, Finland's population is actually 5.5 billion, not million; we just like to stay undercover that way 18:40:38 back 18:40:54 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 Sgeo: Ah yes, Luke Plant. 18:41:21 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 A creationist Christian. 18:41:33 Not someone to rely on to be anything other than a blithering moron. 18:41:57 I've read some of the drivel on his blog occasionally, and it's all that. 18:42:14 I've found myself demotivated when writing C# >.> 18:42:23 So don't use shitty languages 18:44:21 C# is good at that. 18:44:34 It's not all that unique. 18:44:47 It's just an imperative language with objects. 18:45:59 And we've got plenty of those 18:46:14 Too many. 18:46:19 0 18:46:20 woops 18:46:37 sorry guys I didn't mean to!!!! 18:46:41 In this case, alise is probably right 18:46:42 The Expression Problem may have solutions handling both rows and columns, but adding columns is far more valuable than rows. 18:46:49 So to hell with OOP. 18:46:56 oh still on the expression problem?? 18:47:07 alise you know you can do BOTH in haskell? 18:47:09 errr 18:47:11 -!- jcp has quit (Read error: Connection reset by peer). 18:47:15 EITHER* 18:47:29 like, data Exp = Num Int | Add Exp Exp | ..., then write functions on it 18:47:43 Okay: I WILL finish this dependent typer. 18:47:52 At least, before tomorrow; then I won't be able to. 18:47:54 or data Exp = Exp { eval :: Exp -> Int ; show :: Exp -> String, ... }, then write constructors for it 18:48:00 hmm 18:48:16 I got my record syntax wrong but just delete the "Exp ->"'s 18:48:23 -!- jcp has joined. 18:48:57 alise won't be happy until he can make functional circuitry 18:50:47 alise I wrote a dependent type checkr once but the type system was inconsistent 18:51:03 well not inconsisent 18:51:11 but it didn't have subject reduction 18:51:20 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 [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 i'm wayyy out of my league :D 18:57:48 at least you got the pronoun right 18:58:13 10:48:57 alise won't be happy until he can make functional circuitry 18:58:19 no, the reduceron is fine :P 18:58:28 circuitry is functional 18:58:29 event based 18:58:33 this sparks -> other thing 18:59:13 check' vs (L t _) = return t 18:59:14 it'll do for now 18:59:21 after all, you wouldn't lie to me, would you? 18:59:23 Hm 18:59:31 Why were my Chrome extensions all uninstalled? 18:59:38 Because you touch yourself at night. 19:02:03 Oh, dear. 19:02:12 Inferring variables will be hard, as in I haven't accounted for this. 19:02:23 don't infer anything :P 19:02:25 it's too difficult 19:02:35 Well, not infer. 19:02:39 But I have to keep track of variable's types. 19:02:52 yes that's the type context 19:02:59 Yes, and I'm not doing that, you see. 19:03:04 Wait, yes I am. 19:03:07 Uh. 19:03:08 Sort of. 19:03:26 (A aT rT) <- check' vs f 19:03:31 okay, so I need to do it in the lambda-checking clause 19:04:00 check' vs (N x) = Nothing 19:04:02 shouldn't matter for now! 19:04:21 *Main> check SetSet 19:04:22 Just * 19:04:23 ^_^ 19:04:28 *_* 19:05:28 *Main> check idL Just (*) -> (t) -> dt *Main> check (idL :. idL) Nothing 19:05:30 Spot why I can't do that 19:07:17 fff 19:07:19 so many interdependencies 19:07:53 (idL :. (* --> *)) :. idL ? 19:08:12 no, idL :. typeofidL :. idL 19:08:15 what's dt? 19:08:29 de bruijn; t = 0, dt = 1, ddt = 2, etc 19:08:30 t = top 19:08:30 oh hehe you are right 19:08:32 d = dip 19:08:44 the value of the argument of that type is pushed for the RHS of -> 19:08:58 which incidentally means that evaluating your whole program in the typechecker is trivial :) 19:09:10 there's no IO so it doesn't matter 19:12:33 10:47:29 like, data Exp = Num Int | Add Exp Exp | ..., then write functions on it 19:12:34 10:47:54 or data Exp = Exp { eval :: Exp -> Int ; show :: Exp -> String, ... }, then write constructors for it 19:12:40 this + typeclasses might allow for both? 19:14:44 alise I don't want to say no but I dont see it 19:14:57 yeah i was just thinking that typeclasses solve... most problems 19:15:02 anyway your dependent solution doesn't require dependentness 19:15:07 type families = type-level functions, i bet you could do it with those 19:15:24 I am sure that my way make essential use of full spectrum dependent types 19:15:33 what was Snoc again? 19:15:47 Snoc was just an explanative device 19:16:06 you don't have to implement it that way, infact I think I realized a slightly better form 19:16:26 but it's all the same idea 19:16:44 what was the better form? 19:16:47 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 MissPiggy: you know how the f gets the rest of the list? 19:19:57 f?? 19:19:57 what information does it need to make the ROW/COL decision? 19:20:01 the number of rows and the number of cols, right? 19:20:03 f in Snoc f 19:20:25 plus the types of the cols 19:20:30 and the rows 19:20:32 well if you just have a matrix n m, then functions row : matrix n m -> vector n -> matrix n (S m) 19:20:42 and col : matrix n m -> vector m -> matrix (S n) m 19:20:50 I wonder if I got my n/m row/col right way around 19:20:59 I've forgotten the definition of snoc :( 19:21:02 meh 19:21:07 yeah you can forget about snow 19:21:19 Snow! 19:21:20 snoc* 19:22:31 PIGGEHHHHH 19:23:31 "matrix : nat -> nat -> *" is a simplification though.. the real thing would be a bit more involved 19:23:45 so what would a table tarpit be, I wonder 19:23:47 hmm 19:23:50 do nested tables make sense? 19:24:27 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:40 well 19:26:48 nested table doesn't really mean anything 19:26:56 the only reason you'd need to think about multiple tables is: 19:27:03 either you have more than a 2D programming problems 19:27:04 MissPiggy: how been 19:27:20 or you have some kind of mututally recursive system of 2D programming problems 19:27:24 (or both!) 19:27:38 mutualy recursive infinite dimensional progarmming sounds hard thuogh 19:27:49 hey augur I was listening to the space flight remix 19:28:00 WOSSAT :O 19:28:00 live mission was on soma 19:28:11 hows it going with ? 19:28:13 you 19:28:15 oooh right! the launch this morning 19:28:27 is good with me 19:29:17 :) 19:29:42 augur me and ehird solved the exeprssion problem using deptypes 19:29:48 once and forall! 19:29:53 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 AND i created the page http://en.wikipedia.org/wiki/Head_grammar 19:30:11 augur, I still need to get back to CCGs... 19:30:26 oh you edited them 19:30:36 whats the expression problem? 19:30:38 cool I will reread 19:31:05 augur you've done really good with these!! 19:31:25 well for all but the CCG one all i did was add the equivalency note, and some examples for LIG 19:31:30 the head grammar page is all new tho 19:33:13 Wait, there's a new version of Haskell? 19:34:01 Sgeo: what 19:34:07 Haskell 2010 19:34:23 oh, yeah. 19:34:28 new spec 19:35:17 MissPiggy: link augur to my pastie about the expression problem 19:35:18 OR I WILL 19:35:31 D: 19:35:34 http://pastie.org/812459.txt?key=cadkhg4ho0qiceepz1a7w 19:35:59 lol 19:37:56 Yeah; GHC doesn't implement it yet, though. 19:38:07 (won't be too long -- most of what's not done is syntax tweaks) 19:39:07 alise: interesting problem! 19:39:26 yeah MissPiggy came up with a nice solution 19:39:57 my solution would be, do like haskell does, but allow discontinuous definitions of function alternatives. 19:40:15 preprocess it to all be continuous, if desired. 19:41:08 She does that. 19:41:24 augur: Anyway, that still doesn't let you add constructors to a data type. 19:41:35 true 19:42:07 but your link doesnt specify that as necessary, does it? 19:42:16 Yes, it does. 19:42:18 That's what adding a row is. 19:42:28 oh, right, because for haskell you'd have to have them all the same datatype 19:42:32 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:33 union types! 19:42:44 The whole point is that they're the same type 19:42:59 type classes! 19:48:04 -!- znerc has joined. 19:49:18 btw, guys, if anyone wants papers from JSTOR or ACM let me know 19:52:49 im also off to target. BYE 19:55:35 bye 20:02:43 asd 20:03:31 MissPiggy: you'd think that typechecking and evaluating the dependently-typed lambda calculus would be really simple... 20:03:45 it seems like one of those "inherent" concepts that should be really simple to express 20:03:50 no I wouldn't 20:03:54 well 20:03:54 i would 20:04:14 there is a simple (dependently typed) lambda calculus, and that's quite easy to implement 20:04:20 but it's not quite good enough 20:04:35 howso 20:05:41 well you know how types are equal if they are definitionally equal 20:05:55 like: Vector (1 + 1) = Vector 2 20:06:13 one annoying thing is if you don't have eta conversion, then stuff like 20:06:29 exists Nat (\x -> P x) is not convertible with exists Nat P 20:06:34 yeah 20:06:37 x :: Set(x) 20:06:38 f x :: Set(f) = (y::T) -> S, Set(x) = T, y = x, S 20:06:38 now that's just a minor annoyance, 20:06:42 \(x::T) -> ... :: S :: (x::T) -> S 20:06:43 -!- gm|lap has joined. 20:06:44 (x::T) -> T :: * 20:06:47 * :: * 20:06:53 ^ the dependent lambda calculus i'm trying to implement 20:07:27 but there's more to be said about this which is sort of detailed 20:07:44 I assume 20:07:45 (x::T) -> T :: * 20:07:47 actually means, 20:07:56 it's syntax :: type 20:07:58 T :: *, T' :: * |- (x::T) -> T' :: * 20:08:22 well that's nto quite right still 20:08:25 but it's closer :P 20:08:38 (x::T) -> S :: Set(T) = *, Set(x) = T, Set(S) = *, * 20:09:31 Gamma |- x :: T <=> Gamma(x) = T 20:10:11 yeh i was just writing it quickly in the form it came into my head 20:11:13 data Syntax = Var Integer | App Syntax Syntax | Lambda Syntax Syntax | Arrow Syntax Syntax | Set 20:11:23 the semantics is just (Semantics -> Semantics), right? 20:11:29 or does it have Var Integer too 20:12:56 hmm 20:13:00 can my thingy type \x->x x? 20:13:05 i don't think so 20:13:07 there's no a = a -> b 20:13:31 Semantics = Semantics -> Semantics is a good first approximation 20:13:42 but to implement quote it needs to be fudged around a bit, nothing major 20:16:43 cons ∈ (α ∈ ★) → (β ∈ ★) → (γ ∈ ★) → (α → β → γ) → γ 20:17:17 cons ∷ (α∷★) → (β∷★) → (γ∷★) → (α → β → γ) → γ 20:17:21 Still think the latter looks nicer 20:17:35 cons : (α:★) → (β:★) → (γ:★) → (α → β → γ) → γ 20:17:37 looks good too, though 20:17:40 I think the last is best 20:17:45 brb 20:20:02 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 eww. eww. eww. what kind of language is that 20:36:23 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:45:56 it's oklo the pol! 20:46:21 almost no relation to prozac the bear 20:48:12 -!- MissPiggy has joined. 20:55:09 gm|lap: functional, bitch 20:55:34 not very functional when you don't have loonycode 20:55:44 also, some mathematicians definitely were involved. 20:55:49 gm|lap: the 90s called 20:55:56 they want you to stop using windows 20:56:42 it really depends on the situation as to whether using unicode is a good idea or not. 20:57:11 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 as in, an fread of some sort. 20:57:26 gm|lap: Ah, you still think a string is a char *. 20:57:33 You still think C defines the world. 20:57:37 here you'd use an int * 20:57:43 You still think stone-age computing rules over mathematics. 20:57:51 if C was good enough for the romans... 20:57:56 In short, you're the computer-science equivalent of a dinosaur. 20:58:12 hey, at least i know how to code stuff which runs fast 20:58:20 i usually don't, but nevertheless i can. 20:58:25 Except considering how fast computing changes, you're especially Ludditish. 20:58:29 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 as in wildly successful, and survived for > 200 million years 20:58:54 Ha! You think hand-written asm written by _anyone_ other than a genius can beat modern C compilers? 20:58:57 ASM will always be "potentially faster", by the way. 20:59:01 I thought you'd at least stop at C, a vaguely defensible position. 20:59:28 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 i haven't seen ASM from many "modern C compilers" but usually they're bashing at memory 20:59:48 well 20:59:52 This may in fact end up being the most tedious two-way about computing I've ever seen. 20:59:54 from the code I've seen 20:59:58 gm|lap: you are clearly ignorant of modern optimisation techniques 21:00:16 Good luck manually performing intense intraprocedural optimisation 21:00:54 what!!!!!!!!!!!!!!! 21:01:02 I might be more polite if I didn't know there were so many like you. 21:01:06 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 Did I just miss some conversation or was that a non-sequitur? 21:01:30 MissPiggy: All your base is cool again? 21:01:34 EXCELLENT 21:01:37 well, it may help you understand my thinking 21:01:50 No, not really. 21:01:57 I like open things too. 21:02:18 a 4KB demo using libraries to run itself is technically cheating 21:02:23 oerjan: should I read Triangle and Robert? 21:02:35 but of course! 21:02:39 although if you want to be pedantic, i could whip up some code to turn 80x25 into mode 13 21:02:45 w/o INT 0x10 21:02:53 oerjan: but. so many comics 21:03:14 sure, but you're planning to live forever, aren't you 21:03:50 i'd like to, that doesn't mean i think it's going to happen :P 21:04:07 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:08 my base 21:04:33 gm|lap: HA! You think functional programming, which is literally identical to mathematics and logic, is some new-fangled thing? 21:04:43 It's imperative programming that was the unfortunate blip in the history of calculation. 21:05:15 i know that functional programming isn't insanely recent at all 21:05:32 UTF-8 is definitely more recent than functional programming, though 21:05:39 heck, you can even do OOP in ASM 21:05:48 But the symbols I am using are ancient. 21:05:50 can functional programming be liberated from the von noymann parradime? 21:05:56 Ugh, you know what, this really is the most tedious conversation I've had. 21:06:15 imperatives aren't new-fangled either, see kant 21:06:20 Especially as I'm returning to hell tomorrow, I don't feel the need to continue to perpetrate irritated boredom on myself. 21:06:24 oerjan: Har. 21:07:03 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 [21:07] == IGNORE Unknown command 21:07:36 Damn you, webchat.freenode.net. 21:08:46 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 I'm being a wonderful asshole. 21:09:05 yes, and my ignore list is wonderfully persistent. 21:09:22 who is gm?? 21:09:25 are you new 21:09:27 GreaseMonkey. 21:09:27 * gm|lap == Greasemonkey 21:09:29 erm 21:09:29 ohh 21:09:31 GreaseMonkey 21:09:32 He's been irritating for a few years now. 21:09:43 alise: i don't remember you 21:09:47 it does feel like years, doesn't it? 21:09:50 except from, ooh, a few days ago 21:09:51 always greasing up the place 21:09:51 lol 21:09:59 gm|lap: i've been here a long while. 21:10:18 MissPiggy: it has been years; 2006, according to the wiki 21:10:32 oerjan: why did you fuck with it! 21:10:54 what other names would you have used? 21:11:11 alise: wait, what? 21:11:16 Johnathan, Omaha, Harpsichord, Robotic Overloard #3.9, Bob. 21:12:13 ... don't really ring a bell 21:12:46 alise: see history 21:12:51 Also ᚠᚡᚢᚣᚤᚥᚦᚧᚨ. 21:15:10 when i have a piece of paper, i deal with numbers. 21:15:17 when i have a piece of code, i deal with bytes. 21:15:38 I thought you were using your wonderful ignore list. 21:15:50 Please do, I'm uninterested in your drivel and if it would stop you talking to me that would be great. 21:15:55 yes, even though i code in languages which deal with all sorts of numbers, with and without decimal points 21:16:08 hmm, i actually have some power here... 21:17:23 In a world... where one man... must face his demons... 21:17:25 For he has... 21:17:30 THE POWER TO ANNOY 21:17:36 In cinemas feb 14 21:18:31 on the other hand you have the power to be condescending 21:18:41 Wait, you deal with *bytes* in your programs? 21:18:46 I deal with *values*. 21:18:52 Maybe if my life was any better and you were any less idiotic I would not be trolling you. :) 21:18:52 I deal with *stars* 21:19:06 Oh, and morphisms in the category Hask. 21:19:20 i do actually deal with values, but when it comes to files, i have to deal with bytes 21:19:33 Files! Another wonderfully retarded blip in history. 21:19:48 what's wrong with files? 21:19:55 I want to try plan 9 21:20:02 a bunch; maybe i'll explain sometime when I'm not having fun with an idiot 21:20:03 MissPiggy: Made perfect sense when C was unusually high-level. 21:20:07 i tried it, it's easy to break the GUI 21:20:11 That's been a few decades now. 21:20:13 MissPiggy: plan 9 is the closest to making files bearable 21:20:21 it basically makes them universal identifiers in tuple-space 21:20:33 Review of Plan 9 21:20:36 don't you mean plan 9 is the closes to making all bearables files? 21:20:36 It's easy to break the GUI. 21:20:36 - 21:20:41 LOL 21:20:46 Hey, now that was actually funny. 21:21:32 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 That is to say, tedious and pointless. 21:21:57 oh okay 21:22:06 there's quite a difference between english and japanese, so to speak. 21:22:07 so like 21:22:27 you want a "filesystem" that's actually storing data structures instead of just files in a tree 21:22:43 so it would be like a tree of trees instead of a tree of files? 21:22:45 something like that 21:22:46 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:51 well... 21:22:57 I want a "filesystem" to just mean data structures that are persistent. 21:23:00 and allows you hierarchical, non-hierarchical, tagged, searched and everything organisation simply through creating data structures 21:23:19 I'd love for my IO to consist of "persist(foo)". 21:23:19 pikhq: Persistent data structures? Why, what redundancy! 21:23:27 it sounds very difficult to organize 21:23:32 alise: what happened to amend? 21:23:41 MissPiggy: If you want a tree structure, like a symlinkless filesystem, just create it. 21:23:42 No harder. 21:23:49 If you want symlinks, use references. 21:23:55 If you want a searchable pool, do it. 21:23:58 alise: it's not going to make itself 21:24:11 gm|lap: That's why my main field of study is focused on making it. 21:24:16 right. 21:24:36 MissPiggy: Are you familiar with Smalltalk? 21:24:46 An apology for the rather harsh bluntness, by the way; I'm grumpy right now. 21:26:24 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 the question is, what am i confusing arrogance with? 21:27:26 ugh 21:27:57 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 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:14 wait... silly me 21:31:21 roughly half-speed ._> 21:31:27 didn't notice the mixing rate 21:31:47 1.9.0 is pretty slow though 21:35:30 -!- MissPiggy has joined. 21:40:38 there's a package in ubuntu called "sl" 21:40:52 if you type sl accidentally, it suggests that you install it 21:41:03 apt-cache search sl | grep ^sl gives us this: 21:41:04 sl - Correct you if you type `sl' by mistake 21:41:22 25.3kB apparently 21:41:26 *facepalm* 21:41:50 dude you should totally install it, it's awesome 21:42:00 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 Testing, testing, one two three. 21:46:34 sl is just annoying IMO. 21:46:37 I never make that typo anyway. 21:47:00 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 Maybe there should be a carrot, getting ls right speeds up your system for a few minutes or something. 21:48:09 apparently sl is short for "steam locomotive" 21:48:43 Yes; it's a rather terrible pun. 21:48:59 Damn, my XChat looks civilised. 21:51:12 http://imgur.com/CQv7v.png 21:51:20 I'd show the window borders, but apparently gnome-screenshot and scrot fail at compiz. 21:52:13 DejaVu Serif is actually a pretty nice serif. 21:56:35 well dejavu is nice but we've seen it all before 21:57:23 Tabs?? 21:57:31 Erm, button-tabs? 21:58:25 Beats a huge tree with only two lines. 21:59:29 URW Palladio L is also a nice font. 22:04:19 So, value-level (∀a.b) is (λa.b). What's value-level (∃a.b)? 22:04:37 a*b 22:04:47 (a,b) 22:04:49 anything like that 22:05:10 Really? 22:05:21 Hmm. 22:05:23 I guess you are right. 22:05:54 MissPiggy: What about the literal (∃a.a)? 22:06:19 what about it?? 22:06:35 What does that translate to as a value? 22:06:40 If you replace exists with forall, that's id in value-land. 22:07:07 (a,a) sholud work, but also (a,a') 22:07:22 it doesn't have to be the same a 22:07:42 Right, but those would be specific as. 22:08:11 Perhaps my question simply makes no sense :P 22:11:44 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 or something close to that 22:12:58 but if there is no typeclass, only the value is necessary 22:13:14 Actually, (exists a. a) is 0 bits... 22:13:28 really? 22:13:28 You don't need to store the value because the only information you can extract from it is that it exists. 22:13:46 um no 22:13:50 No? 22:13:50 seq, remember 22:13:54 Oh. 22:14:03 Well, seq and unsafePerformIO are not "really Haskell". :) 22:14:10 "Really Haskell" is defined as the subset of Haskell that makes sense. 22:14:11 seq is official 22:14:20 The committee is wrong. 22:14:50 alise: unsafePerformIO, FWIW, only exists as part of the FFI. 22:15:45 i think the new 2010 revision modifies that though 22:15:47 http://bennyhillifier.com/?id=mwDKMiAfxFE 22:16:00 Top of the two bots in the Google Tron AI competition, fighting. 22:16:01 Where can I see the changes in 2010? 22:16:02 To Benny Hill. 22:16:17 http://hackage.haskell.org/trac/haskell-prime/ 22:16:57 *Two of the top 22:17:12 The link on that page seems broken 22:17:14 data Exists (T : *) (P : T -> *) where 22:17:23 Witness : (t : T) -> P t -> Exists T P 22:17:33 MissPiggy: Ah, dependent typists. Always writing everything in the language. 22:17:46 dependent typists :D 22:17:48 -!- tombom_ has quit (Quit: Leaving). 22:18:11 The Cult of Dependent Typists & their Honourable Languages Thereof, est. 1980 22:18:19 (I don't really know how old dependent types are.) 22:18:20 :P 22:18:28 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 doesn't Agda supposedly have both? 22:19:29 I don't think there's any issue with having both. 22:19:33 I just don't really like typeclasses all that much. 22:19:49 agda doesn't have typeclasses 22:19:50 I know that Ur does it with implicit module parameters matching a certain signature. 22:19:55 That's a nice solution. 22:20:03 it's sort of weird because I'm not sure if you can actually add typeclasses 22:20:25 I mean you can pass them explicitly but that probably doesn't count 22:20:26 oh right didn't oleg do something proving the equivalence of modules and type classes. 22:20:31 _+_ : {a:Set} -> {Num a} -> a -> a -> a 22:20:44 Num : Set -> ModuleSignatureThingy 22:20:51 Or something like that. 22:20:53 * MissPiggy has been playing with Ur today 22:20:58 (functorial modules, presumably) 22:20:59 And the implementation: 22:21:25 _+_ {_} {n} x y = n._+_ x y 22:21:27 Or something. 22:21:29 You get the idea. 22:21:49 alise, working link please? 22:21:57 -!- kar8nga has quit (Remote host closed the connection). 22:21:57 the problem with that is you still need the compiler to choose (ARBITRARITLY!!) a Num instance for a 22:21:59 To what? http://bennyhillifier.com/?id=mwDKMiAfxFE? 22:22:15 MissPiggy: same with values that belong to multiple sets in foralls! 22:22:18 It has to pick one! 22:22:26 Sgeo: http://bennyhillifier.com/?id=mwDKMiAfxFE 22:22:29 the final ? breaks it 22:22:33 yeah 22:22:35 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:38 it's scary stuff 22:22:49 Sgeo: oh. 22:22:52 just google haskell prime or w/e 22:23:08 MissPiggy: Well, it picks the most specific type it can infer, right? 22:23:14 Most specific set. 22:23:14 Of a value. 22:23:16 For a forall. 22:23:33 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 Perhaps more functions explicitly implemented. 22:23:58 Or more concrete types. 22:24:06 If there are two equally-specific ones, you must manually specify one. 22:25:18 basically 22:25:21 * oerjan finds a picture of oleg. i never thought of him as that old! 22:25:24 the whole thing about typeclasses is SYNTAx 22:25:34 oerjan: link 22:25:36 and you can't add them without hacking the compiler 22:25:37 I imagine him as a 30-something guy 22:25:41 just being so fucking cool 22:25:49 no employer, he just has money, buys stuff, you know 22:25:50 and what's so good about them anyway, modules are probably better 22:25:53 but mostly just sits around, publishing 22:26:10 oh wait, that's another guy with the same! 22:26:10 MissPiggy: cayenne has no modules because its products (records) are powerful enough to serve as it 22:26:12 as one 22:26:14 oerjan: :) 22:26:17 oerjan: I think he's a private fello 22:26:20 s/$/w/ 22:26:27 ("Oleg Kiselyov, director of Influenza Research Institute") 22:26:34 MissPiggy: so if modules are better than typeclasses 22:26:40 maybe we just need cayenne records and that's it! 22:27:02 hehe 22:27:12 so how you implement records? :) 22:27:22 ohh 22:27:22 * Sgeo is now an Early Edition addict 22:27:31 I like that idea 22:27:35 http://www.cs.chalmers.se/~augustss/cayenne/ 22:27:36 ask them 22:27:40 hey, it's augustss 22:27:45 didn't know he did cayenne!! 22:27:49 Oleg works for the navy 22:28:00 doesn't he ? some kind of waterry thing 22:28:28 http://www.cs.chalmers.se/~augustss/cayenne/examples.html 22:28:32 cayenne's printf implementation is slick 22:28:34 heck wikipedia? "Oleg Kiselyov (born 11 January 1967) is a Russian handball player." 22:28:41 HAND EGG 22:29:22 egghand? 22:30:40 MissPiggy: I think cayenne records are basically haskell records 22:30:42 except automatically typed 22:30:57 like the type of {foo=3,bar=\a->a} is {foo::Int,bar::a->a} or whatever 22:31:10 also I realised something 22:31:16 my dependent LC doesn't have any way to extract an arrow 22:31:19 (the only composite type) 22:32:14 think I should add it? Maybe it could be a built-in function 22:32:36 destarr : * -> c -> (a -> b -> c) -> c 22:32:51 what does extract an arrow mean though? 22:33:02 (a -> b) => (a,b) 22:33:27 I could add pattern matching, but that'd be the only thing it'd be useful for 22:34:53 hm this _might_ be him, http://www.flickr.com/photos/eelcovisser/283343950/ (it is in a computer scientists set) 22:35:21 Personal home page: Paul Kelly 22:35:21 Paul H J Kelly. Professor of Software Technology, Group Leader, Software Performance Optimisation Department of Computing (map); Imperial College London ... 22:35:22 same guy? 22:35:30 oleg is the one in blue 22:35:33 btw 22:36:14 ok so you're sure? it was the only plausible picture on the first page of google hits for "oleg kiselyov" 22:36:19 it's his only t-shirt http://video.google.com/videoplay?docid=-7990603720514207956&ei=OkBvS7SkMovL-AbZwtHjBg&q=oleg+# :) 22:36:27 (picture search) 22:37:33 i guess that crushes my theory he is trying to keep his real appearance secret 22:38:12 oerjan: do keep in mind that the pictures and videos are not necessarily of the actual oleg 22:38:25 olsner hah it's just a puppet! 22:38:25 hm? 22:38:37 MissPiggy: indeed, just a puppet 22:38:43 ah 22:39:26 ((λ:(★ → 0 → 1). 0) (λ:(★ → 0 → 1). 0)) (λ:(★ → 0 → 1). 0) 22:39:31 there's another picture of Oleg on this http://www.angelfire.com/tx4/cus/people/index.html 22:39:50 xD 22:40:11 Guy Steele 22:40:12 Scheme / CL / Fortress 22:40:15 yeah, just ignore the whole Java thing 22:40:21 hehee 22:40:41 MissPiggy: i already knew about that one 22:40:42 MissPiggy: 22:40:43 ((λ:(★ → 0 → 1). 0) (λ:(★ → 0 → 1). 0)) (λ:(★ → 0 → 1). 0) 22:40:46 does that make sense to you? 22:41:12 it was part of what started my conspiracy theory, after all 22:41:17 it's id id id? 22:41:20 yeah 22:41:21 but it wouldn't typecheck 22:41:24 why not 22:41:30 oh 22:41:31 the types 22:41:31 yeah 22:41:50 i can't do implicit arguments without full inferring can i :( 22:41:59 there is no 'full inferring' 22:42:07 it's undecidible 22:42:12 i know 22:42:13 but i mean 22:42:17 "lots" of work inferring 22:42:24 as opposed to some cheap trick 22:42:25 -!- adam_d has joined. 22:42:26 the best you can do is make a powerful algorithm that works well in normal situations 22:42:35 well, check does return the type 22:42:36 but ehhh 22:42:42 well there are some small classes of inference you can do in a principled way 22:42:56 all i care about is inferring type arguments :) 22:42:57 but it's very hard work.. and I think you probably need HOU to even get started 22:43:04 maybe that's easier still 22:43:11 I think I could fake that since my typechecker returns a type it knows it is 22:43:14 but eh 22:43:36 ((((λ:(★ → 0 → 1). 0) (★ → 0 → 1)) (λ:(★ → 0 → 1). 0)) (★ → 0 → 1)) (λ:(★ → 0 → 1). 0) 22:43:36 There. 22:43:38 id id id 22:44:03 * alise writes cons out of sheer insanity 22:44:32 a:* -> b:* -> a -> b -> c:* -> (a -> b -> c) -> c 22:45:50 consL :: Syntax 22:45:50 consL = 22:45:50 Lambda (Arrow Set (Arrow Set (Arrow (Var 1) (Arrow (Var 1) ...)))) $ 22:45:50 Lambda (Arrow Set (Arrow (Var 1) (Arrow (Var 1) ...))) $ 22:45:51 Lambda (Arrow (Var 1) (Arrow (Var 1) ...)) $ 22:45:52 Lambda (Arrow (Var 1) ...) $ 22:45:54 this is getting boring fast :P 22:46:17 not to mention confusing 22:46:17 hm 22:46:23 yeah it's pretty confusing 22:46:44 okay so after c:*... what the fuck number is a 22:46:48 4 22:46:52 b is 3 22:46:53 c is 0 22:47:02 of course that'll change with the arguments of the function :D 22:47:05 (just add one) 22:50:06 foo3.hs:29:132: parse error on input `)' 22:50:07 AIEEEEEEEEEEEEe 22:50:42 λ:(★ → ★ → 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:50:43 MissPiggy: ^ 22:50:55 im not debugging that :P 22:51:01 i need more parens 22:51:08 write a function called --> that turns names into indices 22:51:18 and the opposite way, too 22:51:19 Stupid broken A/V sync on this YouTube video 22:51:22 so I can see what the fuck will happen 22:51:26 so you can write ("x", T) --> "x" instead of T -> #0 22:51:32 λ:((★) → (★) → (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:40 that's cons 22:51:48 now in the sugar language I wrote over this, here's what it'll look like 22:53:03 cons : (α:★) → (β:★) → α → β → (γ:★) → (α → β → γ) → γ 22:53:12 cons _ _ x y _ f = f x y 22:53:32 MissPiggy: actually, if I define some standard representation for a tuple 22:53:47 then I can trivially infer an ((α:★),α) given an α 22:53:56 simply because I must know the type already, since I'm doing typechecking 22:54:50 no? 22:55:27 http://pastie.org/813947.txt?key=s3kxmqh9xb0pvxoycdqzpw 22:55:31 May I never have to write such a thing again 22:55:52 cons ?? 22:56:17 \x y f. f x y 22:56:22 The pair-creator. 22:56:24 yikes O_O 22:56:29 Dependently typed! 22:56:33 why is it so typed 22:56:38 Pretty-printed (ha), it's 22:56:38 jusst make it simple :P 22:56:39 λ:((★) → (★) → (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 MissPiggy: Because I have no other choice. 22:56:47 I have to curry because this is the LC. 22:56:50 * MissPiggy almost spat tea out 22:57:00 But I have to specify the type of every function, because this is no-inferring, typed LC. 22:57:02 through whoms nose 22:57:13 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 My variable names: αβγδεζηθικμνξοπρστυφχψω 23:05:40 they are hot 23:05:50 I love the Greek alphabet. It's beautiful. 23:06:00 I should set it up so that alt-shift types greek 23:06:52 IMAL (In My Awesome Language), typing abcdefg... will automatically convert. :-) 23:07:44 alise: You and your derived-from-Egyptian scripts. 23:08:07 Unicode has up to quadruple prime :D 23:08:48 they don't compose together well, though 23:08:52 different numbers of primes 23:11:43 * MissPiggy thinks unicode is a bit stupid 23:12:54 Why? 23:13:08 It has some stupidities, like the super/subscripts; it shouldn't be trying for a formatting vehicle. 23:13:13 Anyway, behold: 23:13:14 *Main> System.IO.UTF8.putStrLn $ pretty idL 23:13:14 (λ:((α:★) → (β:α) → α))) α. α) 23:13:33 *Main> System.IO.UTF8.putStrLn $ pretty consL 23:13:33 (λ:((α:★) → (β:★) → (γ:α) → (δ:β) → (ε:★) → (ζ:(ζ:α) → (η:β) → ε))) → δ))))))) α. (λ:((β:★) → (γ:α) → (δ:β) → (ε:★) → (ζ:(ζ:α) → (η:β) → ε))) → δ)))))) β. (λ:((γ:α) → (δ:β) → (ε:★) → (ζ:(ζ:α) → (η:β) → ε))) → δ))))) γ. (λ:((δ:β) → (ε:★) → (ζ:(ζ:α) → (η:β) → ε))) → δ)))) δ. (λ:((ε:★) → (ζ:(ζ:α) → (η:β) → ε))) → δ))) ε 23:13:34 . (λ:((ζ:(ζ:α) → (η:β) → ε))) → δ)) ζ. ζ γ δ)))))) 23:13:38 MissPiggy: I hope that clears things up for you. 23:14:03 "(ζ:(ζ:α)" - bug or just plain awesomeness? 23:14:08 I'll go with bug. 23:14:12 PLAIN AWESOME 23:14:24 ζ:ζζζζζζζζ 23:14:26 -!- SimonRC has quit (Ping timeout: 246 seconds). 23:14:38 It's because since you can't technically reference it from inside itself, it's free. :-) 23:16:04 MissPiggy: think I should change the type signatures to (λ(var:type):(result type). )? Not sure if that's actually any better :P 23:16:36 * alise wonders why 23:16:41 let v = ident vs 23:16:42 vs' = v:vs 23:16:45 complains about v not being defined 23:17:43 *Main> System.IO.UTF8.putStrLn $ pretty consL 23:17:43 (λ:((β:★) → (γ:★) → (δ:γ) → (ε:δ) → (ζ:★) → (η:(θ:δ) → (ι:ε) → η))) → ε))))))) α. (λ:((γ:★) → (δ:γ) → (ε:δ) → (ζ:★) → (η:(θ:δ) → (ι:ε) → η))) → ε)))))) β. (λ:((δ:γ) → (ε:δ) → (ζ:★) → (η:(θ:δ) → (ι:ε) → η))) → ε))))) γ. (λ:((ε:δ) → (ζ:★) → (η:(θ:δ) → (ι:ε) → η))) → ε)))) δ. (λ:((ζ:★) → (η:(θ:δ) → (ι:ε) → η))) → ε))) ε 23:17:43 . (λ:((η:(θ:δ) → (ι:ε) → η))) → ε)) ζ. ζ γ δ)))))) 23:17:48 MissPiggy: It's simple, really. 23:17:59 I pity the foo that has to debug their code generator for this 23:19:12 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 *Main> System.IO.UTF8.putStrLn $ pretty (Arrow (Arrow Set Set) (Arrow Set Set)) 23:21:45 (α : (β : ★) → ★) → (β : ★) → ★ 23:21:49 I should probably retain used variables 23:22:14 hmm 23:22:18 this could do with becoming monadic 23:23:10 you mean to make it even more incomprehensible? 23:23:19 * oerjan ducks 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:28:58 alise 23:29:10 have you raed peter morris' work on universe of strictly positive typs 23:34:21 back 23:34:27 no 23:34:46 * alise will implement a new feature in the prettifier 23:34:56 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 *Main> System.IO.UTF8.putStrLn $ pretty idL 23:51:54 (λ(α:★) : (α : α) → *** Exception: List.genericIndex: index too large. 23:52:53 :/ 23:57:57 -!- jcp has joined.