Hacker News Board Hacker News, browsed like a classic message board
Live data from Hacker News

Types

gist.github.com

Post reply on HN
Print view View original

31–40 of 198 posts

Re: Types

#31

Post by titanomachy »

seanwilson wrote: post #29
titanomachy wrote: post #23

Someone who has experience with both Agda and Idris, could you comment on which is easier to get started with? Coming from a Haskell background, I'd like to try my hand at writing more interesting constraints into my types. Any experiences using these languages for (non-research) work? I've played around with Coq a little and it certainly feels more like a proof assistant than a programming language. It was fairly co…

> Someone who has experience with both Agda and Idris, could you comment on which is easier to get started with? Coming from a Haskell background, I'd like to try my hand at writing more interesting constraints into my types. Any experiences using these languages for (non-research) work? The learning curve is almost vertical to be completely honest from personal experience. I find most tutorials are written by people…

> most tutorials are written by people with a strong background in logic, type systems, and mathematics...

I'm a little used to this from Haskell, although I imagine the dependently-typed languages are even worse in that regard. Working through the Idris tutorial now and at least the syntax is familiar.

Re: Types

#32

Post by seanwilson »

catnaroek wrote: post #27
seanwilson wrote: post #26

Earlier quoted context omitted.

> By the way, the idea of deliberately limiting the expressive power of types isn't new: the Damas-Milner type system, which is most certainly known and proven technology, is a first-order subset of System F-omega's type system for which type inference is possible. A dependently typed language with a first-order type level would benefit from reusing the basic architecture of a Damas-Milner type checker: a constraint…

> Have you seen languages like DML (let's you capture linear arithmetic properties only and automates the proof of these)? Yes. But what I have in mind is a little bit more ambitious. I want dependent types restricted to be parameterized by syntactic values (in the sense of ML's value restriction) of what Standard ML calls `eqtype`s. For example, correctly balanced red-black trees would be: (* clearly eqtypes *) data…

Any examples? I'm curious for examples of a nontrivial type that would catch lots of common programming errors where the proofs can be automated. I see lots of new dependently typed languages but not much interest in addressing the proof automation aspect.

Re: Types

#33

Post by catnaroek »

seanwilson wrote: post #32
catnaroek wrote: post #27

Earlier quoted context omitted.

> Have you seen languages like DML (let's you capture linear arithmetic properties only and automates the proof of these)? Yes. But what I have in mind is a little bit more ambitious. I want dependent types restricted to be parameterized by syntactic values (in the sense of ML's value restriction) of what Standard ML calls `eqtype`s. For example, correctly balanced red-black trees would be: (* clearly eqtypes *) data…

Any examples? I'm curious for examples of a nontrivial type that would catch lots of common programming errors where the proofs can be automated. I see lots of new dependently typed languages but not much interest in addressing the proof automation aspect.

I'd love to give more concrete examples, but I'm slightly hampered by the fact the type system I want isn't actually implemented anywhere. I have a rough sketch of the design of the type system I want, and I've been looking for a computer scientist, logician or mathematician to help me polish the design and prove that it is, in fact, type safe. But I couldn't find anyone. :-|

Re: Types

#34

Post by logicchains »

seanwilson wrote: post #11

Great overview article but I have a comment. > In Idris, we can say "the add function takes two integers and returns an integer, but its first argument must be smaller than its second argument": > If we try to call this function as add 2 1, where the first argument is larger than the second, then the compiler will reject the program at compile time. > Haskell has no equivalent of the Idris type above, and Go has no e…

>You don't get this for free and you have to help the computer verify these.

For library types, the most commonly used properties will have already been proven; you wouldn't have to write a proof that "sort" sorts a list any more than you'd have to write the sort function itself.

The computer can also be surprisingly good at proving these things in many cases. E.g. I was playing with the proof assistant Isabelle recently, and I tried to prove that given an int, a proof that twice that int is greater than 13, and a proof that four times that int is less than 29, then that int must be 7. I thought I'd have to fiddle around with induction on Peano numbers and the like, but nope, it could be proved with just a single "by arith".

Re: Types

#35

Post by catnaroek »

logicchains wrote: post #34
seanwilson wrote: post #11

Great overview article but I have a comment. > In Idris, we can say "the add function takes two integers and returns an integer, but its first argument must be smaller than its second argument": > If we try to call this function as add 2 1, where the first argument is larger than the second, then the compiler will reject the program at compile time. > Haskell has no equivalent of the Idris type above, and Go has no e…

>You don't get this for free and you have to help the computer verify these. For library types, the most commonly used properties will have already been proven; you wouldn't have to write a proof that "sort" sorts a list any more than you'd have to write the sort function itself. The computer can also be surprisingly good at proving these things in many cases. E.g. I was playing with the proof assistant Isabelle rece…

> it could be proved with just a single "by arith".

Tactics are probably a usability improvement for mathematicians who are used to proving everything by hand. But for programmers used to type inference, they're a step backwards. Mathematicians typically prove much deeper results, but they do so at a much slower rate than programmers write programs.

Re: Types

#36

Post by seanwilson »

titanomachy wrote: post #31
seanwilson wrote: post #29

Earlier quoted context omitted.

> Someone who has experience with both Agda and Idris, could you comment on which is easier to get started with? Coming from a Haskell background, I'd like to try my hand at writing more interesting constraints into my types. Any experiences using these languages for (non-research) work? The learning curve is almost vertical to be completely honest from personal experience. I find most tutorials are written by people…

> most tutorials are written by people with a strong background in logic, type systems, and mathematics... I'm a little used to this from Haskell, although I imagine the dependently-typed languages are even worse in that regard. Working through the Idris tutorial now and at least the syntax is familiar.

> I'm a little used to this from Haskell, although I imagine the dependently-typed languages are even worse in that regard. Working through the Idris tutorial now and at least the syntax is familiar.

That's what I mean by the difficultly jump. Like when you go from C++ to Java or the other way around, there's a lot of familiar things to cling on to while you make the transition. With dependently typed languages, there's a massive pile of unfamiliar stuff so the steep learning curve is unavoidable really. Someone needs to write a "dependently typed programming for Java programmers guide". :)

Re: Types

#37

Post by wz1000 » 

    add : (x : Nat) -> (y : Nat) -> {auto smaller : LT x y} -> Nat
    add x y = x + y
Actually, (GHC) Haskell can express something like this type if you turn on the required extensions.

    data Nat = Z | S Z deriving (Eq, Ord, Show)
    data SNat (n :: Nat) where
        SZ :: SNat Z
        SS :: SNat n -> SNat (S n)

    type family Compare (a :: Nat) (b :: Nat) :: Ordering where
      Compare Z Z = EQ
      Compare (S a) Z = GT
      Compare Z (S a) = LT
      Compare (S a) (S b) = Compare a b
    
    type a  SNat a -> SNat b -> SNat (a+b)
    add = ...

Re: Types

#38

Post by DanWaterworth »

> Haskell has no equivalent of the Idris type above, and Go has no equivalent of either the Idris type or the Haskell type. As a result, Idris can prevent many bugs that Haskell can't, and Haskell can prevent many bugs that Go can't. In both cases, we need additional type system features, which make the language more complex.

Type checking Idris is much simpler than Haskell.

Re: Types

#39

Post by jroesch »

seanwilson wrote: post #32
catnaroek wrote: post #27

Earlier quoted context omitted.

> Have you seen languages like DML (let's you capture linear arithmetic properties only and automates the proof of these)? Yes. But what I have in mind is a little bit more ambitious. I want dependent types restricted to be parameterized by syntactic values (in the sense of ML's value restriction) of what Standard ML calls `eqtype`s. For example, correctly balanced red-black trees would be: (* clearly eqtypes *) data…

Any examples? I'm curious for examples of a nontrivial type that would catch lots of common programming errors where the proofs can be automated. I see lots of new dependently typed languages but not much interest in addressing the proof automation aspect.

You don't need type theory to verify program properties, people have been using first-order methods for decades to prove properties about programs. For example there was a line of work in ACL2 that verified a microprocessor implementation, as well as plenty of modern work using tools like SMT to automatically prove program properties, see Dafny, F* for language based approaches. Though there is plenty of language agnostic approaches as well. My colleagues at UW have a paper in this year's OSDI verifying crash consistency for a realistic file system with no manual proof.

Re: Types

#40

Post by evincarofautumn »

junke wrote: post #20

1 + eval(read_from_the_network()) > If we get an integer, that expression is fine; if we get a string, it's not. We can't know what we'll get until we actually run, so we can't statically analyze the type. > The unsatisfying solution used in practice is to give eval() the type Any, which is like Object in some OO languages or interface {} in Go: it's the type that can have any value. Values of type Any aren't constra…

> if an expression evaluates without error, then its type is…

What’s curious is that this is true in every language with general recursion/looping:

    int f(int n) {
        while (true) {}
        return n + 1;
    }
(In other words, the type of “f” isn’t the logical formula “a → a”, but rather “a → ¬¬a”.)

The type of “eval” can also be fully static; it can just return a type that you have to do case analysis or runtime type inspection on to use.

In Haskell, with a data type:

    data Value = Integer Int | Text String | ...

    eval :: String -> Value

    foo = do
      value  return (1 + n)
        _ -> error "that was not an integer!"
Or with RTTI:

    eval :: String -> Dynamic

    foo = do
      value  return (1 + n)
        Nothing -> error "that was not an integer!"
“fromDynamic” has the type:

    Typeable a => Dynamic -> Maybe a
Which is to say “given a dynamic value, and its runtime type information, I can either give you the value back with a static type, or nothing if I can’t perform the downcast”—much like “dynamic_cast” on pointer types in C++.
Post reply on HN