4 ms·

Some issues are removed with a type system and wouldn't require writing tests to verfiy (the compiler would be doing this for you). I wouldn't take that fact as

• pauloortins 13y ago
  Type testing can be replaced by static types but you still have to test all the others stuffs in your code.
  • cgag 13y ago
    I just want to note that with an advanced type system, "type testing" can cover a lot more than people seem to give it credit for. An example I saw someone give on here the other day was that he had the types for his red black tree set up so that code that produced an unbalanced tree would never compile.
    • Skinney 13y ago
      Link? How would a type system be able to ensure that both sides of a rb tree is balanced? :S
      • deleted 13y ago
        [deleted]
      • cgag 13y ago
        https://news.ycombinator.com/item?id=5987527 https://news.ycombinator.com/item?id=5987527 I'm just getting into Haskell myself and I can't really explain those 10 lines myself (I also haven't implemented a red black tree). I watched a talk by Yaron Minksy the other day that also talked about the idea that you should "make illegal states unrepresentable" that was really good: http://vimeo.com/14313378 http://vimeo.com/14313378 (he starts talking about that at around ~17:50)
      • tel 13y ago
        Code review time! https://github.com/yairchu/red-black-tree/blob/master/RedBlackTree.hs#L27 https://github.com/yairchu/red-black-tree/blob/master/RedBla... First we create two differently typed tags for Red and Black. data Red data Black Note this differs from something like data Color = Red | Black in that Red and Black are distinct at the type level---the compiler will actually complain if one is used where the other ought to be. Now we state that Trees must have Black roots. This is done using a GADT (Generalized Algebraic Data Type) which allows us to build constructors of types which restrict some of the types. data Tree a where Tree :: Node Black n a -> Tree a For instance, compare PoorTree which would let us make Trees with Red roots data PoorTree c n a = PoorTree (Node c n a) It really does nothing more than wrap up a Node to hide it and change the interface (if you want). Now we need one last piece before digging in to the core. This is the existence of Type-level Naturals. The idea is that, like Red and Black, we introduce two new distinct types, one basic and one parametric. data Zero = Zero data Succ a = Succ a which lets us write (very verbose) naturals like (Succ (Succ (Succ Zero))) == 3 and have the type reflect this exact value (Succ (Succ (Succ Zero))) :: (Succ (Succ (Succ Zero))) (Note this is a little weird, since we can also form the value (Succ 'a' :: Succ Char) which doesn't make much sense. More powerful dependently typed features help here.) Now consider just a branch in the tree, we form that with a simple data type data NodeH l r n a = NodeH (Node l n a) a (Node r n a) which tracks the left and right colors in its type using the l and r type parameters. It also guarantees the constraint that both the left and right child trees have the same black-height. So, if (black3 :: Node Black (Succ Zero) Char) then (NodeH black3 'a' black3 :: NodeH Black Black (Succ Zero) Char). And if (black2 :: Node Black Zero Char) then (NodeH black3 'a' black2) is a compile time type error. So with all these pieces, we can encode the Red/Black criteria directly into our Nodes. Remember already that if we have a Tree it must have the first Node be Black. We can now construct new Nodes in three ways, each of these ways being constrained so as to enforce the balance rules. data Node t n a where -- If we construct a Node with Nil, it forms a leaf. -- Not only are we not allowed to associate left and -- right branches (we don't get to give it a NodeH type), -- we're forced to set the numerical type parameter to Zero ~= 0. Nil :: Node Black Zero a -- If we construct a Node with BlackNode, we can pass a -- subtree with the NodeH parameter, but the type of node we -- get back is necessarily going to increase its height -- since (Succ n) is like (n + 1). BlackNode :: NodeH t0 t1 n a -> Node Black (Succ n) a -- Or we can construct a Red node. In this case, our black-height -- remains unchanged, but we can ONLY do so when we've got a NodeH -- branch with two black subNodes. RedNode :: NodeH Black Black n a -> Node Red n a So, it's a type error to construct a tree in this format which doesn't obey the Red/Black balance rules. Any transformations you write on the tree will be rejected by the compiler if they break the rules.
  • Skinney 13y ago
    Why do people do type testing?
    • tel 13y ago
      It's not type "testing", it's using a strong, static type checking system before compilation as a testing measure. I.e., you never have to write code that asks about types, an automated program simply ensures that the types that your program expresses "make sense together". This is often conflated with type inference where the program code itself is analyzed in order to compute what type it "ought to be". Some combination of type checking and type inference is a powerful, fast, comprehensive tool for encoding how your program ought to behave alongside the program itself.
      • Skinney 13y ago
        Ahh ok. I know this, but got confused when type and testing was included in the same sentence :P
  • nahname 13y ago
    I felt like saying "a minor number of", rather than "Some".