Experimental IRC log happs-2008-04-05

Available formats: content-negotiated html turtle (see SIOC for the vocabulary)

Back to channel and daily index: content-negotiated html turtle

These logs are provided as an experiment in indexing discussions using IRCHub.py, Irc2RDF.hs, and SIOC.

00:20:32<Saizan>MarcWeber: still there? do you have specific questions?
00:23:28<Saizan>it's inspired from HList
00:29:06<MarcWeber>Not yet.. currently reading the GADT paper..
00:29:53<Saizan>oh, a GADT is just a way for contructors to restrict the resulting type
00:30:01<MarcWeber>I've read the HList source (or parts of it) some time ago,, but I've never used GADTs. That' why I can't grasp your code. I think I've figured out how to use it :)
00:32:13<Saizan>so instead of having Nil :: List m l x, we have Nil :: List m Nil x
00:32:41<Saizan>l has been restricted to Nil simply by declaring it in the definition
00:33:15<Saizan>the m parameter of List will always been Index, it's there only because i was experimenting with further generalizations
00:33:19<MarcWeber>One moment..
00:33:55<MarcWeber>When doing pattern matching it's matched against the resulting type of one constructor type definition, right?
00:34:13<MarcWeber> Pair :: Term a -> Term b -> Term (a,b)
00:34:19<Saizan>note that there are two Nil, one is the type Nil i've declared as data Nil, and the other is the constructor for List
00:34:24<MarcWeber>f (Pair a b) = ...
00:35:14<Saizan>that code looks fine, but i don't understand what you're asking
00:35:45<MarcWeber>http://hackage.haskell.org/trac/haskell-prime/wiki/GADTs
00:35:50<MarcWeber>That's the whole example.
00:36:13<MarcWeber>Normal data types look like data Name = Con X Y Z
00:36:26<MarcWeber>Then you match by fname (Con X Y Z) = ..
00:36:58<Saizan>oh yeah, the parameter in the type of the constructor are like the fields of a normal one
00:37:22<MarcWeber>And the Pair constructor is a function returning Term (a,b)..
00:37:48<Saizan>so data Name = Con X Y Z === data Name :: * where Con :: X -> Y -> Z -> Name
00:39:44<Saizan>yeah, so eval (Pair foo bar) :: (a,b) if foo :: Term a and bar :: Term b
00:40:38<MarcWeber>Let's talk about the simple Con X Y Z example..
00:40:39<Saizan>essentially the type parameter can tell you something about the structure of the value
00:40:46<MarcWeber>Con is the type name
00:40:51<MarcWeber>Name is the result.
00:41:01<Saizan>no, Name is the type name
00:41:02<MarcWeber>X -> Y -> Z are parameters
00:41:16<Saizan>Con is a data constructor
00:41:28<Saizan>and yes, those are the parameters
00:41:40<MarcWeber>I'd like to create a Name now.
00:41:47<MarcWeber><something> x y z
00:41:53<MarcWeber>and something is Con then?
00:41:58<Saizan>yes
00:42:35<MarcWeber>unCon (Con x y z) = (x,y,z) ?
00:42:36<Saizan>just like you would do in data Name = Con X Y Z, right?
00:43:53<Saizan>unCon :: Name -> (X,Y,Z) in that case, (we are assuming X, Y and Z stands for some fixed types like Int or Bool etc..)
00:44:28<MarcWeber>yes. That's the type I had in mind..
00:45:37<Saizan>maybe a little useful example will help, typelevel naturals can be defined with data Succ n; data Zero
00:46:08<Saizan>now we want to write vectors, which are just like lists but carry their length in the type
00:47:08<MarcWeber>That Succ stuff is easy. That's used in HList and in haskelldb somewhere to get fixed length strings..
00:47:28<Saizan>data Vex :: * -> * -> * where VNil :: Vec a Zero; VCons :: a -> Vec a n -> Vec a (Succ n)
00:47:47<Saizan>s/Vex/Vec/
00:48:18<Saizan>so you see how Vec works?
00:48:30<MarcWeber>Not yet..
00:49:07<MarcWeber>I'd do something like data a b = a b and data NIL then I can use data XCoord NIL etc
00:49:26<MarcWeber>simple list. And the length is encoded the way it's done in Succ n.
00:49:54<Saizan>yeah, that's a way
00:49:56<MarcWeber>* * * two types in and one out.
00:50:24<MarcWeber>can I write this as data Vex a b where as well ?
00:51:20<Saizan>what is this exactly?
00:51:29<MarcWeber>http://research.microsoft.com/Users/simonpj/papers/gadt/index.htm
00:51:46<MarcWeber>page 1
00:51:54<MarcWeber>data Term a where ...
00:51:58<MarcWeber>next paragraph
00:51:59<Saizan>however in Vec you have two constructor, VNil is for the empty Vec, and so has length Zero
00:52:11<MarcWeber>Equivalently one could write
00:52:20<MarcWeber>data Term :: * -> * where
00:52:39<Saizan>then VCons that takes an element and a Vec of length n, so it gives a Vec of length (Succ n)
00:53:05<Saizan>oh yeah
00:53:28<Saizan>Vec a b and Vec : * -> * -> * are equivalent
00:53:50<Saizan>the kind signature is more explicit
00:53:53<Saizan>imo
00:55:09<Saizan>mostly because 'a' and 'b' are not in scope in the constructors definitions
00:55:31<MarcWeber>; VCons :: a -> Vec a n -> Vec a (Succ n)
00:55:48<MarcWeber>a is the type I want to store, right? Usually Int or Double..
00:56:03<MarcWeber>Vec a n is the Vec I'd like to add another dimension?
00:57:48<Saizan>yes a is the type of the elements
00:58:02<Saizan>adn Vec a n is the tail of the vector you're building
00:58:19<Saizan>VCons is like (:)
00:58:35<Saizan>but also carries the size along
01:00:15<MarcWeber>I just can't imagine where to put the two values of type a and Vec a n in.
01:00:56<Saizan>they are just stored as field of VCons
01:01:42<MarcWeber>without gadt this would be written as VCons a (Vec a n), right?
01:01:47<Saizan>later you can define e.g vhead :: Vec a (Succ n) -> a; vhead (VCons a _) = a
01:01:51<MarcWeber>data ..
01:02:22<Saizan>yeah, you can't really write it without gats, but using a more conventiona syntax it would look like that
01:02:52<MarcWeber>Thanks.
01:03:10<Saizan>conversely if you define data Foo = Con X Y Z, :t Con will give Con :: X -> Y -> Z -> Name
01:03:41<Saizan>err
01:03:42<MarcWeber>Wait. now we have the list head safe thingy somehow.. This
01:03:58<MarcWeber>was given as example somewhere on haskell.org
01:04:09<Saizan>exactly!
01:04:15<Saizan>vhead is a total function
01:05:05<Saizan>no exception can arise, since arguments to it must be of type Vec a (Succ n), so something starting with a Cons
01:05:14<Saizan>err VCons
01:05:24<Saizan>sorry, i keep confusing names..
01:05:59<MarcWeber>You don't have to confuse NIL and V?Cons ;)
01:06:31<Saizan>the type system prevents me to :)
01:07:23<Saizan>however you can still write functions that works on Vec of any size, like a vmap :: (a -> b) -> Vec a n -> Vec a n
01:07:44<Saizan>defined just like the usual map
01:08:10<MarcWeber>That's what you are doing colecting values by Indexes.. but you only return the one matched by type I guess.
01:08:41<MarcWeber>type Ixs1 = (Cons String (Cons Bool Nil))
01:08:42<MarcWeber>type Ixs2 = Cons Int Ixs1
01:09:13<MarcWeber>And this a->b is your update/ insert whatsoever to keep all Maps up to date?
01:09:17<Saizan>those are typelevel lists that contains the types of the indexes
01:10:56<MarcWeber>Fine. I'll try writing this vmap function now.
01:11:11<Saizan>yeah, in change i use map' to update all indexes
01:12:00<Saizan>oh, map' is very similar to vmap, only it's for List
01:13:05<MarcWeber>Another question: To get to know wether an haskell application has space leaks is done by using profiling (AFAIK).. Can HAppS do some checking as well without beeing shut down?
01:14:09<MarcWeber>I mean compare total used memory with count * recordsize .. and if there is a huge difference (maybe 10 times).. there must be something wrong?
01:15:34<Saizan>well if you can get the size of the memory used by the running process you can schedule something like that
01:41:02<MarcWeber>Saizan: Vec :: * -> * where doesn't typecheck, Vec a b where does
01:41:37<MarcWeber>The most confusing thing is that X -> Y -> > looks like a typedef of a function.. But indeed it's only a constructor..
01:43:35<MarcWeber>So maybe data Vec ... where VCons :: a (Vec a n) (Vec a (Succ n)) would have been easier to understand..
01:48:25<MarcWeber>ah no.
03:15:15<int80_h>anyone still on?
03:24:35<int80_h>hello?
07:41:16<MarcWeber>Saizan: Thank you for your explanation tonight. think I've understood your code now. I'll create a small darcs repository called HAppS-ixset-static on my server and add a TODO list. Then I'll start implementing missing features such as unique contstraints, multilevel keys (Map a ( Map b record)) etc.
12:40:08<Saizan>MarcWeber: nice, forking from the HAppS-IxSet repo? so we can merge later?
12:40:29<Saizan>however Vec :: * -> * -> *
12:45:03<MarcWeber>I have to go for lunch. I've started a new one. But it does'nt matter. Of course we can fork the existing one. I shoulde be able to just do darcs pull to get all the other patches. I'll try later
13:07:37<MarcWeber>Mmh I'll try merging in the existing IxSet first
15:39:28<Saizan>MarcWeber: seen my pm?
16:02:45<MarcWeber>Non at all - strange
16:12:49<MarcWeber>I've tried pulling the ixset package two times.. Both times dacrs stopped at patch 162
16:19:57<Saizan>oh, i wasn't identified

Back to channel and daily index: content-negotiated html turtle