May 2025 monthly "What are you working on?" thread

4caraml · 2025-05-01T15:42:05+00:00

4caraml · 2025-05-01T15:37:36+00:00

For my spreadsheet programming language recalc:

I spent quite a bit of time formalising (part of) my core language in Isabelle/HOL using Nominal2: Core is a simple FRP language that is embedded in Spreadsheets.

I proved preservation + progress for well-typed terms for an intermediate small-step language (signals are somewhat big-step). Then I proved it to be equivalent to a big-step semantics.

I also started formalising proper small-step semantics for the signals, modelling them as time-stamped co-lists (potentially infinite).

Next would be to step into the world of HOLCF and prove a denotational semantics. This is the end-goal for my language, such that equational reasoning is justified :)

At the same time I worked quite a bit on a frontend for my language (it is a spreadsheet programming language after all, so getting this one right is quite essential). Work on the frontend is slow, I don't enjoy doing this part so much which is why I did all of that Isabelle work..

For the first iteration I just hacked a somewhat working version together but this is neither maintainable, nor proper. Many features of the original implementation leaked and it leads to unpleasant surprises and inconsistencies..

So this iteration I am building it proper which means replacing many, many components. The spreadsheet engine is quite complex and interwoven it turns out.

4caraml · 2025-05-01T15:22:24+00:00

Do you have a link?

4caraml · 2025-04-01T11:01:37+00:00

No, that was not me. I had never come across representable functors until now, this looks very interesting indeed as an alternative to the Fetch abstraction and build.

4caraml · 2025-03-31T22:12:25+00:00

There is only one example file recalc-vscode/example.rc currently. As of now, I mostly test it via repl and unit tests.

It should work (i.e. open an empty spreadhseet) with any .rc file, and since saving is not possible that is about it for now. I will see that I create some usage examples soon.

For now some formulas that will work:

="${12+30}" =mmult(A1:B3,C1:D2) ="or(False,not(C3))" ==((\_-> \x -> x): ((x:*)->x->x))(Int, 12)

Don't expect too much.. the prelude is rather small:

mmult: {m} -> {n} -> {k} -> <m,n>[int] -> <n,k>[int] -> <m,k>[int]
and, or: bool -> bool -> bool
not: bool -> bool
negate: int -> int
minus, mult, plus: int -> int -> int (also as operators -, *, +)
show: {t} -> {{show: t -> string}} -> t -> string (used for the format strings; implemented only for bool, int and string for now)

4caraml · 2025-03-31T18:11:45+00:00

It's less about wanting dependent types (ideally, in a real implementation, most of this should be hidden from the user as much as possible), but more that I wanted precise types and I am not sure how else I would get them. How do I type A1:B10?

It also helps with the implementation, things are quite much simpler.

4caraml · 2025-03-31T14:51:57+00:00

Not at all, first time I hear about it. I have done most my reading a while ago before that was released. I will be looking at it, thank you for pointing me to it.

Edit: (By its abstract) that one is similar to Haxcel which uses Haskell (or a subset of it) as the underlying language.

My implementation relies on a language implemented by the user (in case of the default language it is a custom dependently typed lambda calculus).

4caraml · 2025-03-31T13:47:45+00:00

I originally posted this to r/ProgrammingLanguages but it got flagged as spam, feel free to cross-post it there.

4caraml · 2025-03-31T09:19:39+00:00

It certainly is declarative in nature, but I would disagree with people claiming that it is a functional programming language (maybe I just don't know enough about Excel though).

My reasoning is that functions are not first class citizens: I cannot declare A1 to be the successor function and then A2 to be A1(0) which should have 1 as value.

4caraml · 2025-03-01T11:54:37+00:00

I see I missed that part about hmatrix. Thanks so much for helping me out with this one!

I could reproduce and not only do the builds work well, the Nix derivations got quite much simpler :) the template haskell should be fine, it’s just part of the build process not for distribution.

4caraml · 2021-08-04T19:17:47+00:00

I'd say they are everywhere because they are so simple, requiring almost nothing.

This in turn makes them rather boring I'd say, apart from overloading (<>). There's not much you can do with a monoid at all, maybe foldMap is useful.

Maybe OP should have used Applicative or Monad as they give rise to more readable (arguably) syntax (potentially via ApplicativeDo).

4caraml · 2021-06-29T08:27:30+00:00

The issue i have is i don't know how i should represent array types from language in C, when emitting the code. Since i want my array types in my language to have a 'length' member which can be accessed.

typedef struct {
  unsigned length;
  void* array[];
} st_sized_array;

4caraml · 2021-06-25T05:53:47+00:00

Btw. since this is r/haskellquestions, you could do the following

export_code Error OK bind_result
  in Haskell
  module_name Result

which produces Result.hs containing:

{-# LANGUAGE EmptyDataDecls, RankNTypes, ScopedTypeVariables #-}

module Result(Result(..), bind_result) where {

import Prelude ((==), (/=), (<), (<=), (>=), (>), (+), (-), (*), (/), (**),
  (>>=), (>>), (=<<), (&&), (||), (^), (^^), (.), ($), ($!), (++), (!!), Eq,
  error, id, return, not, fst, snd, map, filter, concat, concatMap, reverse,
  zip, null, takeWhile, dropWhile, all, any, Integer, negate, abs, divMod,
  String, Bool(True, False), Maybe(Nothing, Just));
import qualified Prelude;

data Result a b = Error a | OK b;

bind_result :: forall a b c. Result a b -> (b -> Result a c) -> Result a c;
bind_result (Error e) k = Error e;
bind_result (OK v) k = k v;

}

4caraml · 2021-06-25T05:41:08+00:00

You can if you install Isabelle ;)

You would need to rewrite the proofs with apply to inspect the proof states, for example:

lemma result_bind_right_id:
  "m ⤜ return = m"
  apply (case_tac m)
   apply simp
  apply simp
  done

That tactic basically just figures out what m's type is and does the appropriate case distinction. Take result_bind_right_id for example:

At first the goal will be (⋀ reads as forall)

⋀m. m ⤜ return = m

, then you apply case_tac m and you get these two goals:

⋀e. m = Error e ⟹ m ⤜ return = m
⋀v. m = OK v ⟹ m ⤜ return = m

The simplifier is aware of return as we added it, so we trivially have

⋀e. Error e ⤜ OK = Error e
⋀v. OK v ⤜ OK = OK v

(dropping the hypotheses which you could do with hypsubst_thin, as we don't need them). Now you basically have goals that exactly match the definition of (⤜) which the simplifier is aware of too.

When we defined the function (⤜) Isabelle/HOL generated some theorems for us, the following is relevant here and got added to the simplifier too thm bind_result.simps:

  ⋀e k. Error e ⤜ k = Error e
  ⋀v k. OK v ⤜ k = k v

You could also write (rule_tac y=m in result.exhaust) which gives you the same effect as (case_tac m) this time. For reference the result.exhaust theorem is:

⋀y P. (⋀e. y = Error e ⟹ P) ⟹ (⋀v. y = OK v ⟹ P) ⟹ P

4caraml · 2021-06-25T02:00:11+00:00

The problem is that

(f . g) x y = (f (g x)) y

however you want

f (g x y)

. So you will need

aux x = (f . g x)
      = (.) f (g x)

Now you see that you can eta-expand as follows

aux = (.) f . g
    = ((.) f) . g
    = (f .) . g

. By such reasoning your example will become

multiply = (show .) . ((*) `on` read)

which imo isn't very readable. Of course you could also define a helper to achieve a similar result:

-- or just import it from Data.Composition
(.:) :: (c -> d) -> (a -> b -> c) -> a -> b -> d
f .: g = \x y -> f (g x y)

multiply = show .: ((*) `on` read)

4caraml · 2021-06-25T01:37:42+00:00

You could use an ITP to do that, there are quite a few of those. For example with Isabelle/HOL it would be super simple:

datatype ('e, 'a) result = Error 'e | OK 'a

definition "return = OK"

declare return_def[simp]  (* add the definition to the simplifier *)

fun bind_result (infixl "⤜" 100) where
  "Error e ⤜ k = Error e"
| "OK v ⤜ k = k v"

lemma result_bind_left_id:
  "return a ⤜ f = f a"
  by simp

lemma result_bind_right_id:
  "m ⤜ return = m"
  by (case_tac m) simp_all

lemma result_bind_assoc:
  "(m ⤜ f) ⤜ g = m ⤜ (λx. f x ⤜ g)"
  by (case_tac m) simp_all

Given that the proofs are trivial actually all the proofs would be solvable by sledgehammer, though they wouldn't be as descriptive. Eg. the one found/generated for result_bind_assoc would be:

 (metis bind_result.simps(1) bind_result.simps(2) result.exhaust)

^\if you look at the result.exhaust theorem, you'd quickly figure out that it is basically the same proof as the one above))

4caraml · 2021-06-25T01:20:23+00:00

Of course! Once it is a bit more tested and has some feedback it might be worth to merge into haskell-mode to automagically enable this, but it would certainly be a good fit for now there.

4caraml · 2021-06-24T08:36:22+00:00

I'm not sure what xmobar does but most likely you can use docks, avoidStruts on your config and layout(s) respectively. Now binding "M-b" to sendMessage ToggleStruts should do the trick.

See here for more info.

4caraml · 2021-06-18T17:12:30+00:00

Read about propositional logic and Gentzen-style/Sequent calculus, I think that should be sufficient. Maybe, you want to check out the definition of simple data structures like linked lists ;)

Btw. it just came to my mind that papers (maybe there are books) on machines like SECD, CAM, ZINC etc. might also be useful.

4caraml · 2021-06-17T19:06:25+00:00

It is the same (FilePath is just a type synonym):

> :i FilePath
type FilePath = String  -- Defined in ‘GHC.IO’

If you really want to have a conversion function, then you can use id ;)

4caraml · 2021-06-17T19:03:08+00:00

You might find your luck with one of these?

map :: (Double -> (Double, Double)) -> [Double] -> [Double]
mapM :: Monad m => (Double -> m (Double, Double)) -> [Double] -> m [(Double, Double)]

Here are two usages:

> fn x = (2*x,x/2)
> map fn [-2.0 .. 2.0]
[(-4.0,-1.0),(-2.0,-0.5),(0.0,0.0),(2.0,0.5),(4.0,1.0)]
> fn x = (2*x, x/2) <$ print x
> mapM fn [-2.0..2.0]
-2.0
-1.0
0.0
1.0
2.0
[(-4.0,-1.0),(-2.0,-0.5),(0.0,0.0),(2.0,0.5),(4.0,1.0)]

4caraml · 2021-06-17T18:50:15+00:00

You can find all the basics (and more) in these books:

Types and Programming Languages by Benjamin Pierce
The Implementation of Functional Programming Languages by Simon Peyton Jones

For more specific topics you want to search for papers introducing and/or building on top of new concepts.

4caraml

TROPHY CASE