4 ms·

Shen more strongly typed than Haskell?

36 points by lkrubner 12y ago

gue5t 12y ago
In short, no, because you can use the same method as discussed of defining a non-empty list type in Haskell, but that data type is not as useful as the regular list type, so it isn't what APIs expect or generate. To have functions which know (in their type signatures) when they'll return empty lists, you need some form of dependent types. In fact, Haskell, in particular GHC with the right set of language extensions, is increasingly capable of implementing various strengths of dependent typing. See http://www.haskell.org/haskellwiki/Dependent_type http://www.haskell.org/haskellwiki/Dependent_type for a discussion of various approaches and a very useful set of links to other resources, some of which discuss this exact use-case.
- salmonellaeater 12y ago
  There is even an example of how to write statically-checked non-empty lists at [1]. [1] http://www.haskell.org/haskellwiki/Non-empty_list http://www.haskell.org/haskellwiki/Non-empty_list
- mbenjaminsmith 12y ago
  As you seem familiar with the topic, can you give me a concrete example of when dependent types would be necessary or useful? If we look at Haskell's Maybe or Swift's option type we have a clear case: There is no ambiguity between an unset variable and a variable set to a null or zero value, i.e., we can clearly express that something isn't there. That allows us to avoid magic numbers as a (horrible) workaround. What do dependent types gain us? [Edit] Rather than clutter up the thread, I'll thank everyone here for the detailed responses below. Really, really interesting stuff. > All of the functions above depend crucially upon the compile time invariant of having a fixed size list. They therefore work for any type-homogenous tuple, for instance, but we'd have to define the functions for each tuple independently. Using `Vect` we can classify the entire family of fixed-sized type-homogenous vectors all at once and dispatch functionality across the whole family. That's pretty much exactly what I was looking for. Thanks again.
  - skybrian 12y ago
    I posted something at top level.
  - gue5t 12y ago
    Looking at Maybe/Option, it's clear that you can write a total function head' :: [a] -> Maybe a. This is good because it allows to represent the function's "failure" to return a head element with an unambiguous, non-magic sentinel value. But really, in many cases you don't want to return "Maybe a" just because you did some operation that involved (somewhere in its middle) taking the head of a list. In some languages you would use "fromJust" or other fundamentally unsafe (in that they can lead the program to terminate abruptly if misused, and in that the compiler cannot help you use them properly) methods to present the interface you want. But ideally, you would have a head function that the compiler would only allow to be called on lists that can be proven non-empty, and which wouldn't need to wrap its return value in Maybe. In a "typical" typesystem, encoding useful information (like how many times you can call tail on a list) into types can be very difficult. For this particular application, you could try to keep track of how many elements are in a list by constructing lists with a generic function that wraps the type it's given in a Cons<T> wrapper, but this approach can run into issues relatively quickly, depending on the language you're using. That said, in some typesystems which aren't fully dependently-typed, you can manage tricks like this, and they can solve this use-case in those contexts. What full dependent types give you is the ability to have types depend arbitrarily on terms (values), such that lists whose types "know their length" are very simple to write, and much more complex guarantees about what your values get up to become possible to implement as types. The downside to this is that running the typechecking algorithm essentially requires arbitrary computation to be performed by the compiler; this can't always be guaranteed to terminate, and may take a few minutes even when it does.
  - tel 12y ago
    A tremendous amount. Everybody's favorite example is fixed-size Vectors. You'd write them like data Vect : (n : Nat) -> (a : Type) where [] : Vect 0 a _::_ : a -> Vect n a -> Vect (n+1) a and then we could statically ensure things like being incapable of taking the head of an empty Vect head : Vect (succ n) a -> a -- even if n = 0, succ n = 1 Or, more cleverly, ensuring that two Vect append to their summed length (++) : Vect n a -> Vect m a -> Vect (n+m) a But the real fun begins with things like "unsequencing" seq : Vect n (a -> b) -> (a -> Vect n b) unseq : (a -> Vect n b) -> Vect n (a -> b) Try to write that with plain lists [0] and you'll find that you are missing certain information about the inputs which make it impossible to do such that seq and unseq are mutual inverses. You can define "zippy" `Applicative` instances for Vect which are not necessarily infinite (unlike List's ZipList instance). Also notice that the following definition of (<star>) is complete despite missing some "obvious" pattern matches... they can never arise and the types ensure it. instance Applicative (Vect n) where pure a = {- elided, but notice that this is tricky -} [] <*> [] = [] (f :: fs) <*> (x :: xs) = f x :: (fs <*> xs) We can also write a Traversable instance instance Traversable (Vect n) where traverse inj [] = pure [] traverse (a :: as) = (::) <$> inj a <*> traverse as and then we can get an "obvious" matrix transposition function type Matrix n m a = Vect n (Vect m a) transpose : Matrix n m a -> Matrix m n a transpose = traverse id All of the functions above depend crucially upon the compile time invariant of having a fixed size list. They therefore work for any type-homogenous tuple, for instance, but we'd have to define the functions for each tuple independently. Using `Vect` we can classify the entire family of fixed-sized type-homogenous vectors all at once and dispatch functionality across the whole family. As a final, much more sophisticated trick, we can look into why that seq/unseq bit worked. Essentially, what we have is that Vect n a is isomorphic with the function Vect n a ~ (Fin n -> a) In other words, it's a function from the finite set of size `n` to values `a`. If we assume some isos and `flip` up : Vect n a -> Fin n -> a dn : (Fin n -> a) -> Vect n a flip : (a -> b -> c) -> (b -> a -> c) then we can write seq/unseq trivially seq : Vect n (a -> b) -> (a -> Vect n b) seq v a = dn (flip (up v) a) unseq : (a -> Vect n b) -> Vect n (a -> b) unseq f = dn (flip (up . f)) In a dependently typed language you can not only create types with these kinds of properties, express the isomorphism above, work generally over these kinds of structures, but you can even generalize the notion of "container" types, types which are functions from a particular shape to their values, in a way that is far more expressive than Haskell would allow. --- And to be honest, all of the above are sort of silly examples. Far more sophisticated type invariants are routinely encoded in DT languages. It's hard to even begin talking about what's going on there. [0] http://stackoverflow.com/questions/25654641/is-it-possible-to-write-a-function-in-haskell-r-a-r-a/25655429#25655429 http://stackoverflow.com/questions/25654641/is-it-possible-t...
skybrian 12y ago
Haskell and similar languages are pretty hard to read for the beginners, so let me give some background: As I understand it, the idea behind dependent typing is to safely separate a runtime check from the code that relies on the check. A runtime check can be done early in the dataflow and only done once (or at compile time for a constant), rather than repeatedly re-checked each time a function uses a value, and the compiler proves this is safe. For this to work, we must encode what we've proven (for example, the length of a list) into the return type at the time we do the runtime check. (Or for a constant, the compiler can calculate the type and we can remove the runtime check altogether.) A very simple sort of check is just to make a NonEmptyList type and ensure that it can only be constructed if the list is non-empty. Everything downstream can rely on this with no runtime check at all. But I'm not sure this even counts; it seems like you need to encode more than one bit of data to make it a dependent type. A more interesting example might be an unzip function that returns two lists that are proven to be the same length. In a regular programming language, the unzip function could return an EqualLenghtListPair type and then you could pass both lists around together, never having to check if their lengths are equal again. But the number of special-purpose types you need gets awkward fast so this isn't really practical without language support.
- tel 12y ago
  That's not really dependent typing. All of your examples are attainable without dependent types. data NEL a = NEL a [a] nel :: [a] -> Maybe (NEL a) nel [] = Nothing nel (a:as) = Just (NEL a as) data EqLen a b = EqLen [a] [b] unzip :: [(a,b)] -> EqLen a b unzip [] = EqLen [] [] unzip [(a, b):rs] = let EqLen as bs = unzip rs in EqLen (a:as) (b:bs) A dependently typed language can of course do these things (the most popular of them are strict supersets of HM languages after all) but generally they would use dependent types to construct richer and more flexible typing invariants.
  - skybrian 12y ago
    Well sure, that was my point. It seems like, even without dependent types, you could do a runtime check to prove anything you like in a type's constructor, and then other code can rely on it being true. But that doesn't mean it's practical to introduce a new type for every possible assertion, nor is the compiler assisting you very much with your proof.
tel 12y ago
I'm not totally familiar with Shen's syntax, but it looks like something interesting is going on here. In particular, the judgement `pop` is being automatically inferred and shown as impossible on the empty list. This is somewhat significantly more powerful than the similar Haskell technique. I'm not sure how Shen's type system works---perhaps some kind of subtyping is at play? Note, that power is a tradeoff in type systems. Typically, greater power can be beneficial for encoding more sophisticated predicates into the type system... but it'll almost certainly have consequences. Normally, power leads to a loss of inference, a need to pass around more type information to prove your claimed types, and/or loss of totality. Whether the power is worth it depends upon your domain.
- bravura 12y ago
  Can you elaborate upon in which domains that power is worth it? And when it is not?
  - tel 12y ago
    As a polarizing example—proof assistants use dependent typing. Their goal is to express interesting mathematical theorems as types and then finding typechecking programs constitutes as proof of those theorems. They absolutely want power and richness over inference---you probably wouldn't want to write a program with an inferable type anyway. It would be too boring.
deleted 12y ago
[deleted]
jrapdx3 12y ago
The comparison of Shen and Haskell caught my eye since Shen was mentioned in HN a few days ago, and I was looking into it. Since I've used Scheme and a port of Shen runs under Chibi Scheme, I wondered what error would show up in Scheme. If I manage to get Shen working (under Chibi) it will be even more interesting to see what it does. Translating, the original problem was: (if (null? xs) (cdr xs) xs) So: (define (mytl xs) (if (null? xs) (cdr xs) xs)) And: (mytl '()) Error: (cdr) bad argument type: () It appears (mytl) emits a type error in this instance. This is obviously a run-time error, and without specific effort I don't think it would be known at compile-time in the Scheme implementations I'm familiar with. Since the Scheme expression appears to embody the semantics of the original problem, I'm inclined to think it shows an underlying difference in the handling of the null list between CL and Scheme implementation I used. If I'm completely wrong, and I can't rule out that possibility, I hope someone will point in the right direction.
- tel 12y ago
  Oh! That's a runtime error... that changes everything.
- tizoc 12y ago
  In Scheme asking for the car or cdr of an empty list is an error, and in Common Lisp it isn't (the result is the empty list itself). In Shen you have "hd" and "tl" which use whatever the platform provides (in Scheme it is going to fail, in Common Lisp it is going to return the empty list), and "head" and "tail" which work the same on all platforms (it is an error to pass an empty list to them, just like in Scheme). > If I manage to get Shen working (under Chibi) it will be even more interesting to see what it does. What problems are you experiencing? Please submit an issue on Github and I will look into it.

36 points by lkrubner 12y ago

gue5t 12y ago

In short, no, because you can use the same method as discussed of defining a non-empty list type in Haskell, but that data type is not as useful as the regular list type, so it isn't what APIs expect or generate. To have functions which know (in their type signatures) when they'll return empty lists, you need some form of dependent types. In fact, Haskell, in particular GHC with the right set of language extensions, is increasingly capable of implementing various strengths of dependent typing. See http://www.haskell.org/haskellwiki/Dependent_type http://www.haskell.org/haskellwiki/Dependent_type for a discussion of various approaches and a very useful set of links to other resources, some of which discuss this exact use-case.

salmonellaeater 12y ago
There is even an example of how to write statically-checked non-empty lists at [1]. [1] http://www.haskell.org/haskellwiki/Non-empty_list http://www.haskell.org/haskellwiki/Non-empty_list
mbenjaminsmith 12y ago
As you seem familiar with the topic, can you give me a concrete example of when dependent types would be necessary or useful? If we look at Haskell's Maybe or Swift's option type we have a clear case: There is no ambiguity between an unset variable and a variable set to a null or zero value, i.e., we can clearly express that something isn't there. That allows us to avoid magic numbers as a (horrible) workaround. What do dependent types gain us? [Edit] Rather than clutter up the thread, I'll thank everyone here for the detailed responses below. Really, really interesting stuff. > All of the functions above depend crucially upon the compile time invariant of having a fixed size list. They therefore work for any type-homogenous tuple, for instance, but we'd have to define the functions for each tuple independently. Using `Vect` we can classify the entire family of fixed-sized type-homogenous vectors all at once and dispatch functionality across the whole family. That's pretty much exactly what I was looking for. Thanks again.
- skybrian 12y ago
  I posted something at top level.
- gue5t 12y ago
  Looking at Maybe/Option, it's clear that you can write a total function head' :: [a] -> Maybe a. This is good because it allows to represent the function's "failure" to return a head element with an unambiguous, non-magic sentinel value. But really, in many cases you don't want to return "Maybe a" just because you did some operation that involved (somewhere in its middle) taking the head of a list. In some languages you would use "fromJust" or other fundamentally unsafe (in that they can lead the program to terminate abruptly if misused, and in that the compiler cannot help you use them properly) methods to present the interface you want. But ideally, you would have a head function that the compiler would only allow to be called on lists that can be proven non-empty, and which wouldn't need to wrap its return value in Maybe. In a "typical" typesystem, encoding useful information (like how many times you can call tail on a list) into types can be very difficult. For this particular application, you could try to keep track of how many elements are in a list by constructing lists with a generic function that wraps the type it's given in a Cons<T> wrapper, but this approach can run into issues relatively quickly, depending on the language you're using. That said, in some typesystems which aren't fully dependently-typed, you can manage tricks like this, and they can solve this use-case in those contexts. What full dependent types give you is the ability to have types depend arbitrarily on terms (values), such that lists whose types "know their length" are very simple to write, and much more complex guarantees about what your values get up to become possible to implement as types. The downside to this is that running the typechecking algorithm essentially requires arbitrary computation to be performed by the compiler; this can't always be guaranteed to terminate, and may take a few minutes even when it does.
- tel 12y ago
  A tremendous amount. Everybody's favorite example is fixed-size Vectors. You'd write them like data Vect : (n : Nat) -> (a : Type) where [] : Vect 0 a _::_ : a -> Vect n a -> Vect (n+1) a and then we could statically ensure things like being incapable of taking the head of an empty Vect head : Vect (succ n) a -> a -- even if n = 0, succ n = 1 Or, more cleverly, ensuring that two Vect append to their summed length (++) : Vect n a -> Vect m a -> Vect (n+m) a But the real fun begins with things like "unsequencing" seq : Vect n (a -> b) -> (a -> Vect n b) unseq : (a -> Vect n b) -> Vect n (a -> b) Try to write that with plain lists [0] and you'll find that you are missing certain information about the inputs which make it impossible to do such that seq and unseq are mutual inverses. You can define "zippy" `Applicative` instances for Vect which are not necessarily infinite (unlike List's ZipList instance). Also notice that the following definition of (<star>) is complete despite missing some "obvious" pattern matches... they can never arise and the types ensure it. instance Applicative (Vect n) where pure a = {- elided, but notice that this is tricky -} [] <*> [] = [] (f :: fs) <*> (x :: xs) = f x :: (fs <*> xs) We can also write a Traversable instance instance Traversable (Vect n) where traverse inj [] = pure [] traverse (a :: as) = (::) <$> inj a <*> traverse as and then we can get an "obvious" matrix transposition function type Matrix n m a = Vect n (Vect m a) transpose : Matrix n m a -> Matrix m n a transpose = traverse id All of the functions above depend crucially upon the compile time invariant of having a fixed size list. They therefore work for any type-homogenous tuple, for instance, but we'd have to define the functions for each tuple independently. Using `Vect` we can classify the entire family of fixed-sized type-homogenous vectors all at once and dispatch functionality across the whole family. As a final, much more sophisticated trick, we can look into why that seq/unseq bit worked. Essentially, what we have is that Vect n a is isomorphic with the function Vect n a ~ (Fin n -> a) In other words, it's a function from the finite set of size `n` to values `a`. If we assume some isos and `flip` up : Vect n a -> Fin n -> a dn : (Fin n -> a) -> Vect n a flip : (a -> b -> c) -> (b -> a -> c) then we can write seq/unseq trivially seq : Vect n (a -> b) -> (a -> Vect n b) seq v a = dn (flip (up v) a) unseq : (a -> Vect n b) -> Vect n (a -> b) unseq f = dn (flip (up . f)) In a dependently typed language you can not only create types with these kinds of properties, express the isomorphism above, work generally over these kinds of structures, but you can even generalize the notion of "container" types, types which are functions from a particular shape to their values, in a way that is far more expressive than Haskell would allow. --- And to be honest, all of the above are sort of silly examples. Far more sophisticated type invariants are routinely encoded in DT languages. It's hard to even begin talking about what's going on there. [0] http://stackoverflow.com/questions/25654641/is-it-possible-to-write-a-function-in-haskell-r-a-r-a/25655429#25655429 http://stackoverflow.com/questions/25654641/is-it-possible-t...

skybrian 12y ago

Haskell and similar languages are pretty hard to read for the beginners, so let me give some background: As I understand it, the idea behind dependent typing is to safely separate a runtime check from the code that relies on the check. A runtime check can be done early in the dataflow and only done once (or at compile time for a constant), rather than repeatedly re-checked each time a function uses a value, and the compiler proves this is safe. For this to work, we must encode what we've proven (for example, the length of a list) into the return type at the time we do the runtime check. (Or for a constant, the compiler can calculate the type and we can remove the runtime check altogether.) A very simple sort of check is just to make a NonEmptyList type and ensure that it can only be constructed if the list is non-empty. Everything downstream can rely on this with no runtime check at all. But I'm not sure this even counts; it seems like you need to encode more than one bit of data to make it a dependent type. A more interesting example might be an unzip function that returns two lists that are proven to be the same length. In a regular programming language, the unzip function could return an EqualLenghtListPair type and then you could pass both lists around together, never having to check if their lengths are equal again. But the number of special-purpose types you need gets awkward fast so this isn't really practical without language support.

tel 12y ago
That's not really dependent typing. All of your examples are attainable without dependent types. data NEL a = NEL a [a] nel :: [a] -> Maybe (NEL a) nel [] = Nothing nel (a:as) = Just (NEL a as) data EqLen a b = EqLen [a] [b] unzip :: [(a,b)] -> EqLen a b unzip [] = EqLen [] [] unzip [(a, b):rs] = let EqLen as bs = unzip rs in EqLen (a:as) (b:bs) A dependently typed language can of course do these things (the most popular of them are strict supersets of HM languages after all) but generally they would use dependent types to construct richer and more flexible typing invariants.
- skybrian 12y ago
  Well sure, that was my point. It seems like, even without dependent types, you could do a runtime check to prove anything you like in a type's constructor, and then other code can rely on it being true. But that doesn't mean it's practical to introduce a new type for every possible assertion, nor is the compiler assisting you very much with your proof.

tel 12y ago

I'm not totally familiar with Shen's syntax, but it looks like something interesting is going on here. In particular, the judgement `pop` is being automatically inferred and shown as impossible on the empty list. This is somewhat significantly more powerful than the similar Haskell technique. I'm not sure how Shen's type system works---perhaps some kind of subtyping is at play? Note, that power is a tradeoff in type systems. Typically, greater power can be beneficial for encoding more sophisticated predicates into the type system... but it'll almost certainly have consequences. Normally, power leads to a loss of inference, a need to pass around more type information to prove your claimed types, and/or loss of totality. Whether the power is worth it depends upon your domain.

bravura 12y ago
Can you elaborate upon in which domains that power is worth it? And when it is not?
- tel 12y ago
  As a polarizing example—proof assistants use dependent typing. Their goal is to express interesting mathematical theorems as types and then finding typechecking programs constitutes as proof of those theorems. They absolutely want power and richness over inference---you probably wouldn't want to write a program with an inferable type anyway. It would be too boring.

deleted 12y ago

[deleted]

jrapdx3 12y ago

The comparison of Shen and Haskell caught my eye since Shen was mentioned in HN a few days ago, and I was looking into it. Since I've used Scheme and a port of Shen runs under Chibi Scheme, I wondered what error would show up in Scheme. If I manage to get Shen working (under Chibi) it will be even more interesting to see what it does. Translating, the original problem was: (if (null? xs) (cdr xs) xs) So: (define (mytl xs) (if (null? xs) (cdr xs) xs)) And: (mytl '()) Error: (cdr) bad argument type: () It appears (mytl) emits a type error in this instance. This is obviously a run-time error, and without specific effort I don't think it would be known at compile-time in the Scheme implementations I'm familiar with. Since the Scheme expression appears to embody the semantics of the original problem, I'm inclined to think it shows an underlying difference in the handling of the null list between CL and Scheme implementation I used. If I'm completely wrong, and I can't rule out that possibility, I hope someone will point in the right direction.

tel 12y ago
Oh! That's a runtime error... that changes everything.
tizoc 12y ago
In Scheme asking for the car or cdr of an empty list is an error, and in Common Lisp it isn't (the result is the empty list itself). In Shen you have "hd" and "tl" which use whatever the platform provides (in Scheme it is going to fail, in Common Lisp it is going to return the empty list), and "head" and "tail" which work the same on all platforms (it is an error to pass an empty list to them, just like in Scheme). > If I manage to get Shen working (under Chibi) it will be even more interesting to see what it does. What problems are you experiencing? Please submit an issue on Github and I will look into it.