Re: Do people who use Ada also use ocaml or F#?

["Chad R. Meiners" <chad.rmeiners@gmail.com>]

On Oct 28, 10:58 pm, Yannick Duchêne (Hibou57)
<yannick_duch...@yahoo.fr> wrote:
> Le Fri, 29 Oct 2010 04:27:40 +0200, Chad  R. Meiners  
> <chad.rmein...@gmail.com> a écrit:> I am love the elegance of static typing
> > without explicit type declarations
>
> Type inference may seems appealing due to its conciseness. Just that as  
> source become bigger, you do not enjoy it any more.

That is the work of a good IDE.  Visual studios does an excellent job
of giving me the type of any variable in F#.  Plus you can also
constrain the parameters ( let x (y : #foo) = ... ) when you want to
prevent certain types of automatic generalization.  Learning Ada's
type system was an excellent introduction how to think about type
systems.

I don't really agree that when the source becomes bigger that type
inference is a problem.  Modules and functors allow you to break up
the system's code so that each piece is understandable, but more
importantly, less work is needed to compose data structures and
functions.

> > Do any other Ada programmers also use functional languages like
> > these?  If so, has anyone given any thoughts on how to incorporate the
> > nice features of both languages?
>
> Ada 2012 introduced something looking like coroutines with the yield  
> function (formally, generators), which is a famous feature of functional  
> paradigm languages (gonna be great for kinds of streams of any kind of  
> data or iterators).
>
> However, adding this and that “cool” feature of that language A in this  
> language B, is easier said than done (you guess?), although this may be a  
> popular topic.

I don't want to add cool features to Ada.  I was thinking more of how
concepts from ML based languages and Ada could be combined to create a
nice statically typed language that would preferably have formal
semantics.  The structural typing of ML makes stuff like

type foo is new Integer range 0..255;

very difficult.   This sort of strong typing with constraints is
something I miss when programming in ML-based languages.  However,
sometimes the verbosity of Ada programs tends towards the
monotonous.   In many cases, the repetition of type assertion is a
desirable sanity check; however, ML-based languages allows for the
functionally to be more efficiently expressed in some cases.  Take
pattern matching and automatic generalization for an example

let reduce foo =
  let rec go carry = function
    | [] -> carry
    | value :: tail -> go (foo carry value) tail
  in go

the equivalent Ada would be (don't have an Ada compiler accessible)

generic
  type t is private;
  type t_list is limited private;
  with function foo(Left : t; Right : t) return t;
  with function head(item : t_list) return t;
  with function tail(item : t_list) return t_list;
  with function isNull(item : t_list) return Boolean;
function reduce(carry : t; list : t_list) return t is
begin
  if isNull(list) then
    return carry;
  else
    return reduce(foo(carry, head(list)), tail(list));
  end if;
end reduce;

It seems to me others may want to combine the nice traits in each
language.  I build research algorithms, conciseness is very desirable
because I want to be able to fit complete algorithms on a page and I
do not want to commit to specific implementations.  However, I want
the compiler to check my type in a rigorous manner so it is easier to
make sure the implementations are correct.

> Cannot reply this question unless you precisely say which feature and for  
> what reason. A lot of job is done by the maintainers (and in some part,  
> the Ada community), to preserve Ada language definition's soundness. Too  
> much risky to talk about adding features just because it sounds cool and  
> buzzy without more reasons (this is not a target). So the question : what  
> feature and for which reason ?

I do not want to change Ada.  I haven't programmed in Ada since 2004.
I might start programming in it again sometime though.

> Honestly, I feel just a few things are missing to Ada, and this have  
> nothing to deal with functional paradigm (which is one among numerous  
> others), as these are more subtilities related to what Ada is already,  
> like the topic of extendable enumerations which pops-up again a few days  
> ago.

Well you can write functional programs in Ada.  It can actually be
quite fun.

> I personally enjoy the paradigm of functional programing (and many others  
> do, the Ada community is open-mind and enjoy to learn to understand), but  
> this is clearly not Ada's target and its principle of least-surprise  
> (predictability). Functional programming better express a modal than a  
> concrete implementation. As I suppose you know, there are many talks about  
> the ability of this/that xML compiler to produce efficient binary  
> application. Ada clearly has nothing to deal with this kind of question,  
> as talks about Ada compilers even goes the opposite way, and more talks  
> about “does that compiler really compiles the input it gets without any  
> error or bad alterations ?”. What you may understand, is that this do  
> exactly the opposite of what a functional programming language compiler is  
> expected to do.

I know the comp.lang.ada is filled with wise and open minded people.
This is why I asked if these wise people have thought of combining
nice features from both languages.

> In shorter words : yes, many people in the Ada world know about FP, its  
> part of their culture; if they use Ada instead of FP (for some things),  
> that is not because they do not know enough about FP; and last, Ada is not  
> and will never be an FP language (but feel free to create an FP compiler  
> targeting Ada).

I know that people here know more than Ada.

> If Ada tends to integrate some features, these are more the one suggested  
> by SPARK users expectations (SPARK is a language intended to run formal  
> proofs of correctness on an Ada program) or by some Ada profiles for  
> short-memory systems, short time response systems, etc. FP does not really  
> help here (well, FP is in some way related to formal proofs, but only in  
> its own language area… adding FP features to Ada will not help to make Ada  
> designs easier to prove).

I know.  I have used SPARK before, and I have built model checker
generator in Ada.  I know a little bit about formal methods ;-p

> Still feel free to tell about your concrete ideas.

I was asking for others' vague and concrete ideas.  It is pretty
difficult to figure out how ML feature and Ada features can be
combined.  I am working on a gut feeling that the combination could be
pretty awesome.  t'class would be pretty nice in an ML language.