How compile a DSL, does it need Types? (Was: Chicken and egg, with curry?)

Hi,
Well you don't need always types. JavaScript
has also no types. And there is a trend to
have gradual types. Make them kind of optional
and arive at TypeScript. If I am not mistaken,
you can omit Types in TypeScript here and then,
and simply get JavaScript. You can still prove things
about, just assume that you have an "any" type. What
other benefit do you think have types? For example
the Floyd Warshall algorithm in DSL works without
any declared types although it has a manifest type
of matrice somehow. Also many Program transformations,
such as the compilation of the DSL doesn't need types.
Here you see the compilation of the DSL,
I just turned the helper predicate into expansion rules:
goal_expansion(let V = E,
    let2(E,V)) :- var(V), !.
goal_expansion(let D[R,C] = E,
   (let2(E,V),
    arg(R, D, H),
    nb_setarg(C, H, V))).
goal_expansion(let2(V, V), true) :- var(V), !.
goal_expansion(let2(D[R,C], V),
   (arg(R, D, H),
    arg(C, H, V))) :- !.
goal_expansion(let2(E+F, R),
   (let2(E, V),
    let2(F, W),
    R is V+W)) :- !.
goal_expansion(let2(V, V), true).
goal_expansion(if E > F,
   (let2(E, V),
    let2(F, W),
    V > W)).
Sadly I don't have yet goal expansion in Dogelog Player. But
SWI-Prolog has it. I might introduce it in the next release
provided I find an ultra simple solution. Or an inline directive.
Bye
The SWI-Prolog thread was this:
https://swi-prolog.discourse.group/t/floyd-warshall-algorithm-in-prolog/8685?u=j4n_bur53
Julio Di Egidio schrieb:

On 03/01/2025 22:14, Mild Shock wrote:
 

Not sure whether this helps. But I think it could help
nevertheless:
>
- i) Logic Programming is the Egg
>
- ii) From the Egg Turtles or Chickens can hatch,
     its very easy to program functionally or
     procdurally in Prolog. Just add small DSLs:

 I was indeed thinking along that line, though a full-fledged dependently-typed functional language is not a small DSL, and I don't think we can eventually do with less: for expressivity and modularity up to arbitrary "functions" (I am thinking computability logic a la Japaridze here, anyway indeed functional are the *problem* domains) as well as proofs of properties of those "functions".
 -Julio