3 ms·

The non-nullable types are trivially implemented in Haskell. From what I can tell the flow control analysis you're talking about is just type inference (another

by tel 13y ago

The non-nullable types are trivially implemented in Haskell. From what I can tell the flow control analysis you're talking about is just type inference (another thing well tackled in ML-like languages). Indeed, everything you've written can be fairly trivially implemented in Haskell, though inference and annotation would feel different. The real challenge comes in when you've got an arbitrary "test" expression which must be satisfied by the statics of your language. For instance, your original example had ensure blocks ensure { x.left > 10 && x.right < 30 } the problem is that it's very difficult for the compiler to take constraints like these and propagate them through increasingly complex transformations without just representing the entire language at the type level. Which is exactly the path taken by "DT" languages like Agda, Coq, Idris, ATS. The upshot is that you get arbitrarily powerful static queries. The downside is that your type system is exactly as complex as your language itself and you have to shuffle around proofs of various invariants being held because it's an NP-complete search problem for the compiler to find them for itself. I highly recommend trying out Coq if this kind of stuff interests you. I recommend Coq over Agda/Idris because you're going to be learning new syntax anyway and Coq has better literature out there: http://www.cis.upenn.edu/~bcpierce/sf/ http://adam.chlipala.net/cpdt/

captainmuon 13y ago
Thanks, I'll definitely have a look at Coq (well, once I have free time, and I wanted to really understand Haskell first). The thing that bothers me about implementing these constraints the Haskell or Idris way (or in any other DT language I've encountered) is that it feels a lot like template metaprogramming in C++. Define integers with nested types as Zero and the sequence of successors (data Nat = Z | S Nat) seems a lot like defining integers with the Peano axioms using nested C++ templates - possible, even neat, but a bit crazy. Maybe that feeling goes away when you're more familiar with the languages. Btw. I've just found out that Spec# (an extension of C#) almost has what I described... you can define preconditions and invariants that are checked at least at runtime, but a static checker tries to proove as much as possible at compile time. Its a pity it is no longer developed, this could have been the static type checked language for the rest of us: http://rise4fun.com/specsharp/
- tel 13y ago
  If you want to see a dependently typed (technically, though the term often doesn't include this class of languages in practice) language which enforces smaller sets of properties more eloquently take a look at Liquid Haskell http://goto.ucsd.edu/~rjhala/liquid/haskell/blog/about/ http://goto.ucsd.edu/~rjhala/liquid/haskell/blog/about/ The core idea here is called the Refinement Type which is basically what you're looking for. In order to power this type system Liquid Haskell depends on a full SMT solver, though, which is a rather large hammer to wield. As it regards to Peano arithmetic in DT languages the Peano naturals data type is awkward for doing math... but FANTASTIC for defining the properties of recursion and induction. Indeed, what you find is that the Peano nats show up everywhere as being a stable foundation for complex proofs and smart recursive functions. It's a very similar feature to Haskell's lists. Competent Haskell programers do not use lists when they want arrays or vectors—the latter types are naturally far more convenient when in their application space. But lists are not abolished! They're fantastically useful as control structures indicating sequential recursion. Typically you think of data types as forming their meaning through construction. You use numbers by constructing them according to arithmetic properties. Another way to do it, though, especially with recursive ADTs and inductive families, is to think of a type's meaning as being derived from how you break it down. The canonical way to break down a list is to find some way of combining the head of the list with the broken-down version of the tail of the list. In Haskell that is called foldr -- combiner zero list result foldr :: (a -> b -> b) -> b -> [a] -> b and you can see its canonicity by thinking of it as simply replacing the constructors for a list by the arguments to foldr. let ls = Cons 1 (Cons 2 (Cons 3 Nil))) foldr comb zero ls = comb 1 (comb 2 (comb 3 zero)))

by tel 13y ago

captainmuon 13y ago

Thanks, I'll definitely have a look at Coq (well, once I have free time, and I wanted to really understand Haskell first). The thing that bothers me about implementing these constraints the Haskell or Idris way (or in any other DT language I've encountered) is that it feels a lot like template metaprogramming in C++. Define integers with nested types as Zero and the sequence of successors (data Nat = Z | S Nat) seems a lot like defining integers with the Peano axioms using nested C++ templates - possible, even neat, but a bit crazy. Maybe that feeling goes away when you're more familiar with the languages. Btw. I've just found out that Spec# (an extension of C#) almost has what I described... you can define preconditions and invariants that are checked at least at runtime, but a static checker tries to proove as much as possible at compile time. Its a pity it is no longer developed, this could have been the static type checked language for the rest of us: http://rise4fun.com/specsharp/

tel 13y ago
If you want to see a dependently typed (technically, though the term often doesn't include this class of languages in practice) language which enforces smaller sets of properties more eloquently take a look at Liquid Haskell http://goto.ucsd.edu/~rjhala/liquid/haskell/blog/about/ http://goto.ucsd.edu/~rjhala/liquid/haskell/blog/about/ The core idea here is called the Refinement Type which is basically what you're looking for. In order to power this type system Liquid Haskell depends on a full SMT solver, though, which is a rather large hammer to wield. As it regards to Peano arithmetic in DT languages the Peano naturals data type is awkward for doing math... but FANTASTIC for defining the properties of recursion and induction. Indeed, what you find is that the Peano nats show up everywhere as being a stable foundation for complex proofs and smart recursive functions. It's a very similar feature to Haskell's lists. Competent Haskell programers do not use lists when they want arrays or vectors—the latter types are naturally far more convenient when in their application space. But lists are not abolished! They're fantastically useful as control structures indicating sequential recursion. Typically you think of data types as forming their meaning through construction. You use numbers by constructing them according to arithmetic properties. Another way to do it, though, especially with recursive ADTs and inductive families, is to think of a type's meaning as being derived from how you break it down. The canonical way to break down a list is to find some way of combining the head of the list with the broken-down version of the tail of the list. In Haskell that is called foldr -- combiner zero list result foldr :: (a -> b -> b) -> b -> [a] -> b and you can see its canonicity by thinking of it as simply replacing the constructors for a list by the arguments to foldr. let ls = Cons 1 (Cons 2 (Cons 3 Nil))) foldr comb zero ls = comb 1 (comb 2 (comb 3 zero)))