Mr. Hui, It's an honor. If I stay to only total functions then my code is guaranteed to be either productive or guaranteed to terminate. Knowing that my program will never "crash" if I remain disciplined is a good starting point. Modulo infinite recursion and dirty data, but apparently Haskell can "solve the halting problem" with a <<loop>> exception, by doing some simple code path analysis, which I rarely, if ever bump into. For the sake of utility you can define partial functions as well, since working with a language with only total functions would not be very fun.
The other thing that can increase my confidence is the fact that you wrap primitive data types with newtype wrappers among other type-level invariances. So if you have a UserID and a PostID, you can wrap Ints with these wrappers and ghc will distinguish at compile time between the two and won't accept any code that mixes up the two. Even though both have the exact same representation at run time with the wrappers being completely erased. To contrast this with some issues, mainline Haskell lumps all IO into a single monad. You can do things like Eff: http://hackage.haskell.org/package/extensible-effects that let you to break up the IO monolith into even smaller effects. So I know from the type that this function will open the water valves and not fire the missiles, instead of all being lumped into a single IO monad. Although mainline Haskell has not fully accepted Eff, or any of the other libraries or proposals yet. The last thing is information flow, Basically you tag a piece of data as private and if attempt to write code that leaks that information out to the real world, the program won't compile. The only way to do it is to coerce the types, implying malicious intent. http://hackage.haskell.org/package/lio http://hackage.haskell.org/package/seclib So although there is no one answer to the confidence question, wearing the hair shirt of strong static types (to me) has some benefits in some cases. The big benefit for me when using J is that if my problem fits into tables, which it does quite a lot, then there is no shorter or quicker way from data to answer than J. I've been thinking about NLP in J too, the high amount of implicit mapping seems like it can be super useful in a variety of cases. J is great for my confidence in correctness because of the fact that it is so dense, it can be obviously correct just by looking at it. J wins on that front by leaps and bounds. Haskell has some of this property too, although it is much more verbose, but a lot of the time you can see that a program is correct, just by looking at it. Unlike many other languages. If it typechecks, all the better! This is usually due to great refactoring capabilities of Haskell. Lazyness and purity allow you to rip out pieces without any change to the code whatsoever, being able to break everything down to its component pieces, usually with lots of whitespacing to emphasize the patterns in the code. If you tried to write Haskell code they way you write oneliners in J, it just wouldn't work, it'd actually be more verbose because you would have to use the fully explicit version with the semicolons and curly brackets to write it all on one line, since indentation is significant in Haskell. About assertions, the way I think about it, is that I would rather think about the problem for a little longer to be able to be able to derive at least some parts of the specification in the types. Now it's also very easy to over-specify and actually make it more difficult. For the things you can't specify (Like hashing functions, etc.) there is always testing, I'm sure you've heard of the famous QuickCheck libary, with it's property based testing: http://hackage.haskell.org/package/QuickCheck There is also tasty, which integrates a whole bunch of testing libraries: http://hackage.haskell.org/package/tasty Thank you Raul, I've heard that happens with explicit definitions, right? If I have my model correct, as soon as you interpret the verb over the data and specialize it to the columns, you are essentially running at the bare metal until the data ends and interpretation continues, specializes, and cycles for more data. On Thu, Apr 2, 2015 at 9:10 PM, Roger Hui <[email protected]> wrote: > In my daily work I program a lot in C, and think a lot in APL/J. IMO, a > type system catches only the easy errors. I mean, if a Haskell program > compiles (passing all the type checks), how confident are you that the > program will work? > > On the other hand, I am a believer in assertions such as demonstrated in > verb LUcheck in http://www.jsoftware.com/jwiki/Essays/LU_Decomposition . > In this case, I am confident that a solution that passes all the assertions > is correct. Assertions tend to be more robust than programs because > testing is typically easier than computing. (e.g. it's much easier to > check that S is a solution to an NP complete program than to derive it.) > > > > On Thu, Apr 2, 2015 at 7:34 PM, Aistis Raulinaitis <[email protected]> > wrote: > > > I'm rather agnostic either way! I like J so much because of it's > dynamism. > > The J does dynamism right, bar none (imo). I only need to say one word, > > rank. I haven't found anything that compares to it in any other language. > > Not even Factor comes close, and I really really like it's stack > > combinators and fried quotations. What I really like about J is that a > lot > > of the work I do fits right into it, quick, iterative, data exploration, > > make a graph and forget about the code forever. No other language lets me > > do that entire cycle as quickly as J, the solution can usually fit in a > > tweet. What I've been thinking about is that there must be some really > nice > > underlying way to give J an optional type system, or at make some sort of > > toy language that fits the bill. That and there is no implementation for > > obverse in Haskell, aka: ^_1 :: (a -> b) -> (b -> a). Although maybe if > you > > add some constraints on a and b and reified J's AST, maybe it would go > > somewhere. My first thought is to do something like: ^_1 :: (JVal a, JVal > > b) => JFunc a b -> JFunc b a. > > > > I know Mr. Iverson really didn't like types, and I completely understand > > that. It can absolutely slow down the development of the language, but > > giving up sum types in J is a bit sad to me. I think that just that would > > be interesting, since nil is horrible and Maybe is bliss, and I think J > > would benefit from having the capability. Then my personal bias shows in > > the fact that I'm sold on dependent types, which I actually think are > > *necessary* for typing some of J's trickier semantics. Such as functions > > that dispatch on the type of the argument. My first thought was to use > type > > level sums, but then I realized that not much work has been done in that > > area. Compound that with the fact that I realized that some functions > would > > require *open* sums, *at the type level*! So that would give up all the > > nice things that closed sums give you. So now my best guess is to track > the > > types with a type level set, and then to dispatch to the proper function > > with that information. So the type would contain the possible types of > the > > arguments that could be passed in, essentially still maintaining 100% of > > the polymorphism (if everything goes right), while also giving you > compile > > time errors if you pass say an int into something that expects an array. > > You could go one step further (and I would), and track the dimensions of > > the array at the type level. So the type of (2D) transpose would be: > > 2dtrans :: [a][b] -> [b][a], where a and b are the length of each > > dimension. Generalized NDimensional transpose would be a little > trickier, I > > think it can be done with enough tinkering. You could then go on and say > > that you expect specific sizes: someFunc :: [3][4] -> [5][4] -> [8][4], > or > > leave some parts polymorphic: otherFunc :: [a][5] -> [6][b] -> > > [(a+b)*3][7]. Yes, that is type level computation, welcome to dependent > > types! ;) It's like ASSERT but even better! > > > > This would essentially give you compile time errors for a whole suite of > > things that usually go wrong at runtime. It would also probably give > better > > error messages, at least more verbose ones. > > > > Very interesting article! > > > > Devon, I hope some of the above answers a part of your question. If you > > already have some experience with Haskell, I would implore you to try a > > dive into Agda. http://oxij.org/note/BrutalDepTypes/ <--- My favorite > > tutorial on Agda. Install Emacs if you don't already use it and use > Agda's > > auto proof search feature, it's a completely different way of programming > > and it's definitely the future in it's own way. If you want a good > example > > of Agda's power, I'll shamelessly promote some of my own code, wherein I > > use Agda to prove some trivial things in physics: > > > > > https://github.com/sheganinans/Static-Dimensions/blob/master/StaticDimensions.agda#L638 > > > > On Thu, Apr 2, 2015 at 6:12 PM, Joey K Tuttle <[email protected]> wrote: > > > > > Lots of topics to chat about ;-) > > > > > > Sorry to say, I don't admire your idealized child - but these things > are > > > indeed personal. > > > > > > In general, choice of language is intensely personal -- e.g. in this > > > story about a fellow "suing himself" over language license issues... > > > > > > http://www.forbes.com/sites/ryanmac/2014/06/05/on-the- > > > > verge-of-ipo-arista-networks-faces-lawusit-from-a-billionaire-cofounder/ > > > > > > I don't know how that ended - but I thought that it was interesting > view > > > of passion for a language. > > > > > > > > > > > > On 2015/04/02 17:01 , Aistis Raulinaitis wrote: > > > > > >> Definitely. Thanks. I felt a little sad for the author's distaste for > > >> static typing. As a Haskeller I actually see static typing as tool to > > lean > > >> into when things get tough, instead of a thing you have to work > against. > > >> To > > >> me programs are just data and mappings of that data from input to > > output. > > >> I > > >> may just be one of those weirdos, but for me (at least right now) the > > >> perfect language for me would be if J and Idris/Agda had a baby and > > made a > > >> dependently typed array language. ...and regained back APL's symbolic > > >> syntax and left ASCII in the dust. > > >> On Apr 2, 2015 4:33 PM, "Joey K Tuttle" <[email protected]> wrote: > > >> > > >> With this interesting article - > > >>> > > >>> http://www.technologyreview.com/review/536356/toolkits-for-the-mind/ > > >>> > > >>> > > >>> > > > ---------------------------------------------------------------------- > > > For information about J forums see http://www.jsoftware.com/forums.htm > > > > > ---------------------------------------------------------------------- > > For information about J forums see http://www.jsoftware.com/forums.htm > > > ---------------------------------------------------------------------- > For information about J forums see http://www.jsoftware.com/forums.htm > ---------------------------------------------------------------------- For information about J forums see http://www.jsoftware.com/forums.htm
