Sorry for the double post. Just remembered: Frames https://github.com/acowley/Frames is an experimental library that came out somewhat recently, among some of its cool features is the function tableTypes, which will read in a csv file and infer the most generic parser that will work for the column. Very nice, I just ask myself why I didn't think of it. :)
On Thu, Apr 2, 2015 at 11:27 PM, Aistis Raulinaitis <[email protected]> wrote: > 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
