logs archiveBotHelp.net / Freenode / #ada / 2015 / July / 22 / 1
Shark8
... https://pastebin.mozilla.org/8840197 (minor improvement/fixes to the opened_/closed_file package; dang OCD-ish itch.)
If you're talking the closed/open file thing, possibly... if the tasks/POs no [IMO].
The former would force a *LOT* of generics all over the place, along with a lot of the logic (which previously was done via subprograms and/or exceptions) pushed into the realm of the type. (Such would be useful for proving, like SPARK, but I think the resultant changes in the program composition would outweigh the benefit.)
^-- ESPECIALLY when you consider SPARK can do that sort of checking w/o forcing such a huge re-archetecting of the program.
darkestkhan
apparently it is possible to make inductive (or rather: recursive) definitions with type_predicates, unless I misunderstood something
Shark8: my solution to Open_File/Close_File doesn't demand that much of rearchitecturing
but still a bit of work... and is less flexible than your generic one
[it is idea only anyway - but as I say "Idea is worth 1000 solutions"]
Shark8
...LOL -- http://stackoverflow.com/a/11910993/608963
darkestkhan
Shark8: https://gist.github.com/darkestkhan/852262b9f3caa9f6d045 this is LOL
Shark8: I don't believe that SO question O_o
Shark8
So... proving that a value in range 0..2**16 is >= 0.
darkestkhan
Shark8: recurrent definition of type ;)
Shark8
It [SO answer] reminds me of an answer I gave to a Ada question [regarding HW] once.
darkestkhan
at least how I understood wiki article about inductive types... prolly misunderstood something
Shark8
Ah, here it is -- http://stackoverflow.com/a/13335859/608963
darkestkhan
"Good Lord! What is this, comp.lang.ada? :-)   Marc C "
made my day
(or rather - night)
Shark8
:) -- It made my day too.
I'm terrible for that answer, aren't I?
darkestkhan
you are talking to a guy who just defined numeric type with predicate that checks if value in range 0 .. 2**16 is >= 0...
by doing recurrent check on 'Pred no less!
(instead of simple >=)
hmm... I wonder if we can do linear type definitions in Ada...
Shark8
Hm, maybe...
darkestkhan
(Action) is getting scared - at this tempo we may end up showing that we have almost every from of type theory covered in one way or other...
*form
s/linear type/specyfikacja arytmetyk liniow/ [linear arithmetic specification]
http://www.ii.uni.wroc.pl/~lukstafi/pmwiki/uploads/Infer/lukstafi-phd-thesis.pdf the work itself is in English [with exception of title xD]
basically type definitions using linear arithmetic - fro example 3*n d 4*k + i [according to my firend who wrote this work multiplying variables is not yet solved]
Lucretia
Visaoni: also, if you don't want dispatching in the api, use pragma Restrictions (No_Dispatching_Calls) https://gcc.gnu.org/onlinedocs/gcc-4.9.3/gnat_rm/No_005fDispatching_005fCalls.html#No_005fDispatching_005fCalls
jk4_
better late than never...
darkestkhan: *shrug* :)
nerdboy
hmm, i suppose if -fsanitize=address makes something compile it's not really a good thing
at least not by itself anyway...
charlie5
!quote
Allegra--
An expert is a person who avoids small error as he sweeps on to the grand fallacy.
-- Benjamin Stolberg
Shark8
darkestkhan: I tried to use generics to emulate the monads here https://www.youtube.com/watch?v=ZhuHCtR3xq8 -- the approach I was trying didn't work... though I think maybe if I tried the type as Type X(<>) is limited private it might.
Here's a blog entry about functional-programming in Ada: http://okasaki.blogspot.com/2008/07/functional-programming-inada.html
And discussion on it at lambda the ultimate: http://lambda-the-ultimate.org/node/2897
wtp
Saw this. http://www.emailgoodies.faketrix.com/pics-office-humor-work-comedy-funny-jobs-picture-5-stress-reduction-kit.htm
Couldn't resist printing one out for fun :D
« prev next »