Shen more strongly typed than Haskell?(groups.google.com)
groups.google.com
Shen more strongly typed than Haskell?
https://groups.google.com/forum/?hl=en#!topic/qilang/LsGvPTtVN9k
21 comments
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.
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.
A tremendous amount.
Everybody's favorite example is fixed-size Vectors. You'd write them like
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.
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
---
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-t...
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
head : Vect (succ n) a -> a -- even if n = 0, succ n = 1
(++) : Vect n a -> Vect m a -> Vect (n+m) a
seq : Vect n (a -> b) -> (a -> Vect n b)
unseq : (a -> Vect n b) -> Vect n (a -> b)
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)
instance Traversable (Vect n) where
traverse inj [] = pure []
traverse (a :: as) = (::) <$> inj a <*> traverse as
type Matrix n m a = Vect n (Vect m a)
transpose : Matrix n m a -> Matrix m n a
transpose = traverse id
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)
up : Vect n a -> Fin n -> a
dn : (Fin n -> a) -> Vect n a
flip : (a -> b -> c) -> (b -> a -> c)
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))
---
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-t...
I really like your examples with the vector whose size is controlled by the type. However, is that useful in practice? I suppose that your vector would be read from a file or a database (especially if you do data analysis), in which case you can't know in advance - at compile time - what size the vectors will have.
I suppose it can still work if you want to do things with the covariance/correlation matrix: you may not know the number of rows before hand, but you know the number of columns, or know that two data sets will have the same number of columns.
I suppose it can still work if you want to do things with the covariance/correlation matrix: you may not know the number of rows before hand, but you know the number of columns, or know that two data sets will have the same number of columns.
The code you write doesn't necessarily fix an n, it just says that n cannot change in unprincipled ways throughout a computation. When you read in a vector from a database it will originally be unsized, but you can write code that shows the size is computed and left fixed and then from then on treat it as a sized vector.
It's hard to say exactly how useful this is in practice. More honestly, this is a rather trivial example mostly used to demonstrate DT.
One use of it is in implementing de Bruijn indexed lambda calculus interpreters---if you let the environment be a sized vector then you can use `n` to ensure there aren't bad variables in scope and to take note of closed expressions.
It's hard to say exactly how useful this is in practice. More honestly, this is a rather trivial example mostly used to demonstrate DT.
One use of it is in implementing de Bruijn indexed lambda calculus interpreters---if you let the environment be a sized vector then you can use `n` to ensure there aren't bad variables in scope and to take note of closed expressions.
The n can come from the database, a file, or even user input from a text box. That's the point of dependent types: types can depend on run-time values.
Well, the n must "come from" the actual data. You could not construct a vector of any other size n. It'll just be typed so as to be realized at runtime and then maintained. The functions by-and-large do not ensure that the vector is sized for a particular n, but instead that they respect whatever n ends up being true.
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.
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.
I posted something at top level.
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
[1] http://www.haskell.org/haskellwiki/Non-empty_list
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.
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.
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)
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.
It's obviously a tradeoff, but dependent types can make the space of these assertion types more rich and also ensure that they are true by construction.
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.
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.
Can you elaborate upon in which domains that power is worth it? And when it is not?
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.
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:
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.
Translating, the original problem was:
(if (null? xs) (cdr xs) xs)
(define (mytl xs) (if (null? xs) (cdr xs) xs))
(mytl '())
Error: (cdr) bad argument type: ()
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.
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.
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.
Oh! That's a runtime error... that changes everything.
[deleted]
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 for a discussion of various approaches and a very useful set of links to other resources, some of which discuss this exact use-case.