#ocaml on 2013-04-16 — irc logs at freenode.irclog.whitequark.org

2013-02-24 19:25 flux changed the topic of #ocaml to: Discussions about the OCaml programming language | http://caml.inria.fr/ | OCaml 4.00.1 http://bit.ly/UHeZyT | http://www.ocaml.org | Public logs at http://tunes.org/~nef/logs/ocaml/

00:00 walter|r has quit [Quit: This computer has gone to sleep]

00:27 darkf has joined #ocaml

00:37 <bernardofpc> does anyone here know how to write an induction on a polymorphic proposition type ?

00:39 <bernardofpc> hum, nevermind, it just works

00:45 talzeus has quit [Quit: Where is the love...]

01:03 Neros has quit [Ping timeout: 264 seconds]

01:15 Nahra has quit [Remote host closed the connection]

01:15 Nahra has joined #ocaml

01:20 madroach has quit [Ping timeout: 248 seconds]

01:21 madroach has joined #ocaml

01:45 venk has joined #ocaml

01:55 breakds has joined #ocaml

02:10 talzeus has joined #ocaml

02:24 talzeus has quit [Remote host closed the connection]

02:27 studybot_ has joined #ocaml

02:36 pkrnj has quit [Quit: Textual IRC Client: www.textualapp.com]

02:58 studybot_ has quit [Quit: where is the love...]

02:58 studybot_ has joined #ocaml

02:59 studybot_ is now known as talzeus

03:30 jophish has joined #ocaml

03:55 jophish has quit [Remote host closed the connection]

04:15 asmanur has quit [Ping timeout: 252 seconds]

04:17 asmanur has joined #ocaml

04:17 derek_c has joined #ocaml

04:24 paddymahoney has quit [Remote host closed the connection]

04:31 ulfdoz has joined #ocaml

04:42 UncleVasya has joined #ocaml

04:53 vpit3833 has joined #ocaml

04:55 venk has quit [Ping timeout: 252 seconds]

04:57 iZsh has quit [Ping timeout: 245 seconds]

05:01 iZsh has joined #ocaml

05:09 Snark has joined #ocaml

05:45 ulfdoz has quit [Read error: Operation timed out]

05:47 breakds has quit [Quit: Konversation terminated!]

05:52 breakds has joined #ocaml

06:06 zpe has joined #ocaml

06:07 vpit3833 has quit [Remote host closed the connection]

06:08 Tobu has quit [Read error: Connection reset by peer]

06:08 Tobu has joined #ocaml

06:16 ttamttam has joined #ocaml

06:19 zpe has quit [Ping timeout: 258 seconds]

06:20 ttamttam has left #ocaml []

06:27 Tobu has quit [Ping timeout: 246 seconds]

06:28 breakds has quit [Quit: Konversation terminated!]

06:31 skchrko_ has quit [Ping timeout: 255 seconds]

06:40 wsebastian has joined #ocaml

06:46 zpe has joined #ocaml

06:48 hkBst has joined #ocaml

06:57 zpe has quit [Ping timeout: 264 seconds]

07:03 anderse has joined #ocaml

07:10 awm22 has quit [Quit: Leaving.]

07:12 ttamttam has joined #ocaml

07:13 ttamttam has quit [Client Quit]

07:18 UncleVasya has quit [Ping timeout: 246 seconds]

07:24 zpe has joined #ocaml

07:24 eikke has joined #ocaml

07:34 zpe has quit [Ping timeout: 255 seconds]

07:35 derek_c has quit [Quit: leaving]

07:40 frogfoodeater has quit [Ping timeout: 264 seconds]

07:41 Kakadu has joined #ocaml

07:48 mika1 has joined #ocaml

07:49 djcoin has joined #ocaml

07:50 mfp has quit [Ping timeout: 256 seconds]

07:51 thomasga has joined #ocaml

07:52 hkBst has quit [Read error: Connection reset by peer]

07:52 hkBst has joined #ocaml

07:52 hkBst has quit [Changing host]

07:52 hkBst has joined #ocaml

07:55 frogfoodeater has joined #ocaml

07:56 eikke has quit [Ping timeout: 252 seconds]

07:57 ontologiae has joined #ocaml

07:58 <ousado> what's a "proposition type"?

08:01 <pippijn> a proposition is the same as a type

08:01 zpe has joined #ocaml

08:01 <pippijn> unless I don't know what you're talking about

08:01 <pippijn> ousado: where did you get this?

08:01 <ousado> pippijn: "[02:37] <bernardofpc> does anyone here know how to write an induction on a polymorphic proposition type ?"

08:02 <pippijn> hm

08:02 <ousado> trying to extract sense from that

08:02 mfp has joined #ocaml

08:03 <pippijn> as I understand it, a proposition is something you say, and consists of proofs about its truth

08:04 <pippijn> and a type is a proposition in that you say "there is at least one value of this type"

08:06 <ousado> hm - not sure a proposition must contain any proof

08:06 <ousado> I think it's just a statement about something

08:07 SuperNoeMan has quit [Ping timeout: 260 seconds]

08:08 jbrown has joined #ocaml

08:08 beckerb has joined #ocaml

08:08 <ousado> http://www.wolframalpha.com/input/?i=proposition

08:10 ia0_ has quit [Quit: leaving]

08:10 zpe has quit [Ping timeout: 258 seconds]

08:11 SuperNoeMan has joined #ocaml

08:14 <ousado> pippijn: but I wonder whether he just means a recursive algebraic data type

08:15 <pippijn> ousado: I think he means sex

08:15 <ousado> pippijn: that's certainly the nicest interpretation

08:15 <pippijn> ousado: see meaning 6

08:15 <ousado> yeah

08:15 ia0 has joined #ocaml

08:21 frogfoodeater has quit [Ping timeout: 246 seconds]

08:27 eikke has joined #ocaml

08:28 awm22 has joined #ocaml

08:32 yacks has quit [Ping timeout: 264 seconds]

08:34 eikke has quit [Ping timeout: 252 seconds]

08:37 zpe has joined #ocaml

08:42 ttamttam has joined #ocaml

08:46 mcclurmc has quit [Ping timeout: 258 seconds]

08:47 zpe has quit [Ping timeout: 252 seconds]

08:50 SanderM has joined #ocaml

08:51 troydm has quit [Ping timeout: 256 seconds]

08:59 Arsenik has joined #ocaml

09:08 yacks has joined #ocaml

09:09 rixed has joined #ocaml

09:14 ollehar has joined #ocaml

09:14 zpe has joined #ocaml

09:22 zpe has quit [Ping timeout: 258 seconds]

09:24 <wmeyer`> ousado: proposition is a type that lives in the proof universe

09:25 <wmeyer`> it defines the set of valid types

09:26 <wmeyer`> but pippijn is right in general when there is no phase separation it's technicaly and semanticaly equivalent to type

09:26 Yoric has quit [Ping timeout: 246 seconds]

09:27 <wmeyer`> in general it's a logical equation that defines the set of types. Whatever the logical system is.

09:32 skchrko_ has joined #ocaml

09:43 malo has joined #ocaml

09:43 mort___ has joined #ocaml

09:46 frogfoodeater has joined #ocaml

09:49 zpe has joined #ocaml

09:52 dsheets has joined #ocaml

09:53 mcclurmc has joined #ocaml

09:57 zpe has quit [Ping timeout: 264 seconds]

10:07 SanderM has quit [Remote host closed the connection]

10:09 RagingDave has joined #ocaml

10:11 beckerb has quit [Ping timeout: 245 seconds]

10:13 Neros has joined #ocaml

10:24 Zerker has joined #ocaml

10:24 zpe has joined #ocaml

10:28 ollehar has quit [Ping timeout: 258 seconds]

10:33 zpe has quit [Ping timeout: 252 seconds]

10:33 Yoric has joined #ocaml

10:37 Zerker has quit [Quit: Colloquy for iPad - Timeout (10 minutes)]

10:38 Zerker has joined #ocaml

10:50 frogfoodeater has quit [Ping timeout: 248 seconds]

10:50 beckerb has joined #ocaml

10:51 Zerker has quit [Quit: Colloquy for iPad - Timeout (10 minutes)]

10:52 dsheets has quit [Ping timeout: 240 seconds]

10:52 Zerker has joined #ocaml

11:00 zpe has joined #ocaml

11:08 zpe has quit [Ping timeout: 245 seconds]

11:14 chambart has joined #ocaml

11:14 ollehar has joined #ocaml

11:31 Arsenik has quit [Remote host closed the connection]

11:34 _andre has joined #ocaml

11:35 zpe has joined #ocaml

11:43 SanderM has joined #ocaml

11:44 zpe has quit [Ping timeout: 264 seconds]

11:45 eikke has joined #ocaml

11:45 cdidd has quit [Remote host closed the connection]

11:47 talzeus has quit [Quit: where is the love...]

11:49 Zerker has quit [Quit: Colloquy for iPad - Timeout (10 minutes)]

11:53 Zerker has joined #ocaml

12:00 dsheets has joined #ocaml

12:01 mort___ has quit [Quit: Leaving.]

12:01 Zerker has quit [Remote host closed the connection]

12:07 dsheets has quit [Ping timeout: 264 seconds]

12:11 zpe has joined #ocaml

12:19 zpe has quit [Ping timeout: 246 seconds]

12:42 yacks has quit [Quit: Leaving]

12:42 chambart has quit [Ping timeout: 258 seconds]

12:43 UncleVasya has joined #ocaml

12:50 zpe has joined #ocaml

12:54 studybot_ has joined #ocaml

12:55 zpe has quit [Ping timeout: 260 seconds]

12:55 dsheets has joined #ocaml

13:00 seymour has joined #ocaml

13:02 breakds has joined #ocaml

13:10 darkf has quit [Read error: Connection reset by peer]

13:10 darkf has joined #ocaml

13:11 yacks has joined #ocaml

13:14 smondet has joined #ocaml

13:16 q66 has joined #ocaml

13:19 seymour has quit [Quit: Saliendo]

13:22 zpe has joined #ocaml

13:30 zpe has quit [Ping timeout: 255 seconds]

13:57 zpe has joined #ocaml

14:06 zpe has quit [Ping timeout: 264 seconds]

14:08 frogfoodeater has joined #ocaml

14:14 studybot_ is now known as talzeus

14:18 chambart has joined #ocaml

14:24 cdidd has joined #ocaml

14:28 mika1 has quit [Quit: Leaving.]

14:33 zpe has joined #ocaml

14:33 dsheets has quit [Ping timeout: 256 seconds]

14:40 frogfoodeater has quit [Ping timeout: 264 seconds]

14:42 zpe has quit [Ping timeout: 256 seconds]

14:50 anderse_ has joined #ocaml

14:51 anderse has quit [Ping timeout: 252 seconds]

14:51 anderse_ is now known as anderse

14:57 darkf has quit [Quit: Leaving]

15:07 tane has joined #ocaml

15:09 zpe has joined #ocaml

15:17 zpe has quit [Ping timeout: 245 seconds]

15:27 ontologiae has quit [Ping timeout: 258 seconds]

15:33 talzeus has quit [Quit: Where is the love...]

15:37 UncleVasya has quit [Ping timeout: 252 seconds]

15:38 eikke has quit [Ping timeout: 256 seconds]

15:45 zpe has joined #ocaml

15:55 zpe has quit [Ping timeout: 276 seconds]

16:04 hkBst has quit [Quit: Konversation terminated!]

16:04 ttamttam has quit [Quit: ttamttam]

16:06 SanderM has quit [Read error: Connection reset by peer]

16:16 beckerb has quit [Ping timeout: 245 seconds]

16:18 eikke has joined #ocaml

16:18 dsheets has joined #ocaml

16:21 zpe has joined #ocaml

16:27 Yoric has quit [Ping timeout: 248 seconds]

16:30 ttamttam has joined #ocaml

16:30 zpe has quit [Ping timeout: 272 seconds]

16:30 dsheets has quit [Ping timeout: 245 seconds]

16:33 Kakadu has quit []

16:35 breakds has quit [Remote host closed the connection]

16:40 mort___ has joined #ocaml

16:46 mort___ has quit [Quit: Leaving.]

16:47 awm22 has quit [Quit: Leaving.]

16:53 eikke has quit [Ping timeout: 245 seconds]

16:57 zpe has joined #ocaml

17:00 anderse has quit [Ping timeout: 252 seconds]

17:06 contempt has joined #ocaml

17:06 zpe has quit [Ping timeout: 256 seconds]

17:09 mcclurmc has quit [Ping timeout: 264 seconds]

17:12 anderse has joined #ocaml

17:12 UncleVasya has joined #ocaml

17:13 contempt has quit [Ping timeout: 256 seconds]

17:17 contempt has joined #ocaml

17:26 eikke has joined #ocaml

17:28 thomasga has quit [Quit: Leaving.]

17:34 Kakadu has joined #ocaml

17:38 zpe has joined #ocaml

17:38 dsheets has joined #ocaml

17:42 zpe has quit [Ping timeout: 240 seconds]

17:49 contempt has quit [Ping timeout: 248 seconds]

17:51 emmanuelux has joined #ocaml

17:59 malo has quit [Quit: Leaving]

18:01 troydm has joined #ocaml

18:09 contempt has joined #ocaml

18:14 contempt has quit [Ping timeout: 245 seconds]

18:17 contempt has joined #ocaml

18:25 weie has quit [Quit: Leaving...]

18:37 Arsenik has joined #ocaml

18:40 RagingDave_ has joined #ocaml

18:44 dsheets has quit [Ping timeout: 264 seconds]

18:44 RagingDave has quit [Ping timeout: 264 seconds]

18:50 smerz_ has joined #ocaml

18:53 RagingDave__ has joined #ocaml

18:53 giaour has joined #ocaml

18:53 giaour has quit [Changing host]

18:53 giaour has joined #ocaml

18:56 RagingDave_ has quit [Ping timeout: 276 seconds]

18:59 malo has joined #ocaml

19:02 <orbitz> does anyone think expanding on my blog posts on using a result type over exceptions is interesting enough for a OUD talk? I think it's probably too simple for your average ocamler.

19:05 RagingDave_ has joined #ocaml

19:08 adahlberg has joined #ocaml

19:08 adahlberg has left #ocaml []

19:08 RagingDave__ has quit [Ping timeout: 255 seconds]

19:10 Trollkastel has joined #ocaml

19:11 <thelema> orbitz: yes, probably too simple

19:11 <thelema> and iirc, it's already been a talk at the ocaml yearly meeting

19:15 <orbitz> looks like i need to work hard to find something interesting to talk about next year

19:16 chambart has quit [Ping timeout: 245 seconds]

19:26 awm22 has joined #ocaml

19:36 thomasga has joined #ocaml

19:39 Kinter has joined #ocaml

19:39 Kinter has left #ocaml []

19:44 ollehar has quit [Ping timeout: 264 seconds]

19:51 giaour has quit [Ping timeout: 260 seconds]

19:51 Yoric has joined #ocaml

19:53 malo has quit [Ping timeout: 245 seconds]

19:57 giaour has joined #ocaml

19:59 ollehar has joined #ocaml

20:00 UncleVasya has quit [Ping timeout: 248 seconds]

20:02 malo has joined #ocaml

20:10 Snark has quit [Quit: leaving]

20:18 chambart has joined #ocaml

20:21 _andre has quit [Quit: leaving]

20:25 Trollkastel has quit [Quit: Brain.sys has encountered a problem and needs to close. We are sorry for the inconvenience.]

20:27 Trollkastel has joined #ocaml

20:36 giaour has quit [Ping timeout: 246 seconds]

20:37 Arsenik has quit [Remote host closed the connection]

20:50 anderse has quit [Quit: anderse]

20:53 ttamttam has left #ocaml []

20:57 wsebastian has quit [Remote host closed the connection]

20:57 djcoin has quit [Quit: WeeChat 0.3.9.2]

21:02 malo has quit [Ping timeout: 252 seconds]

21:09 Kakadu has quit []

21:09 ollehar has quit [Ping timeout: 272 seconds]

21:11 chambart has quit [Ping timeout: 246 seconds]

21:11 weie has joined #ocaml

21:15 malo has joined #ocaml

21:17 malo_ has joined #ocaml

21:17 malo_ has quit [Client Quit]

21:17 dsheets has joined #ocaml

21:30 malo has quit [Ping timeout: 246 seconds]

21:33 malo has joined #ocaml

21:50 mcclurmc has joined #ocaml

21:59 RagingDave_ has quit [Quit: Ex-Chat]

22:03 thomasga has quit [Quit: Leaving.]

22:04 smondet has quit [Ping timeout: 245 seconds]

22:05 Neros has quit [Ping timeout: 258 seconds]

22:07 Neros has joined #ocaml

22:09 malo has quit [Quit: Leaving]

22:12 Yoric has quit [Ping timeout: 252 seconds]

22:33 bobry has quit [Ping timeout: 252 seconds]

22:34 emmanuelux has quit [Ping timeout: 272 seconds]

22:39 tane has quit [Quit: Verlassend]

22:41 dsheets has quit [Read error: Connection reset by peer]

22:48 ollehar has joined #ocaml

23:00 Tobu has joined #ocaml

23:11 frogfoodeater has joined #ocaml

23:12 emmanuelux has joined #ocaml

23:14 ocaml_noob has joined #ocaml

23:18 darkf has joined #ocaml

23:22 q66 has quit [Remote host closed the connection]

23:26 ousado has quit [Ping timeout: 256 seconds]

23:28 ousado has joined #ocaml

23:29 Trollkastel has quit [Quit: Brain.sys has encountered a problem and needs to close. We are sorry for the inconvenience.]

23:31 Trollkastel has joined #ocaml

23:33 jbrown has quit [Ping timeout: 276 seconds]

23:35 Trollkastel has quit [Client Quit]

23:35 frogfoodeater has quit [Ping timeout: 245 seconds]

23:42 smerz_ has quit [Ping timeout: 255 seconds]

23:45 Trollkastel has joined #ocaml

23:47 frogfoodeater has joined #ocaml

23:52 chrisdotcode has joined #ocaml