That may be fine in the abstract, but I would like to know, in the specific
case of the LUP decomposition, how knowing that the types are correct gives
you any confidence that the result is correct. With the assertions in
LUcheck in http://www.jsoftware.com/jwiki/Essays/LU_Decomposition
assert. (($p) -: ,n) *. (i.n) e. p
assert. (($L) -: m,m) *. ((0~:L)<:(i.m)>:/i.m) *. 1=(<0 1)|:L
assert. (($U) -: m,n) *. (0~:U)<:(i.m)<:/i.n
assert. A -: p {"1 L mp U
If these all pass, I am pretty sure that the result is in fact an LUP
decomposition.
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
>
----------------------------------------------------------------------
For information about J forums see http://www.jsoftware.com/forums.htm
