:PROPERTIES: :ID: a4125049-4953-454b-ab18-80b6e0409085 :mtime: 20230924192625 20230924172726 20230923183127 20230923155647 20230922194645 20230922083453 :ctime: 20230922083436 :END: #+title: My Concatenative Langauge #+filetags: :project:public:workproject: * Basic Idea It has been my intention for a long time to design my own concatentative langauge. * Inspiration My language is inspired by the following languages: - [[id:a06fee30-feab-4e30-a32a-ffa7d1dcfc1e][Joy (Programming Language)]] for the concatenative and flat syntax - [[id:0f71a1c3-958b-4895-86b9-33d225a393ea][Agda]] for the formalism and strict adherence to the truth. This language will essentially be Agda but with the syntax of Joy. * Design Principles I want my language to be highly principled. There will be no loosey-goosey features. I think I should look at category theory for a source of formalism. * Innter workings and Implementation Details The hardest part will be how to get such a language to work. * Overloaded space/typeclasses The language will have typeclasses, and space will be a typeclass for composition in a category. For example, this will be valid code #+BEGIN_SRC joy "hello" print "goodbye" print *> : () -> IO () #+END_SRC but this will also be valid code because of the Kliesi Category. #+BEGIN_SRC joy "hello" print "goodbye" print : () -> IO () #+END_SRC * Bisecting typechecking I am pretty sure that typechecking will be the most difficult part of my language to implement. I have an idea which I am calling "bisecting typechecking" will will hopefully lead to linear-time typechecking. (This idea may have been done before, but I am not aware of it) The basic idea is to pick a composition in the middle of the code (thus bisecting the code). If the typeclass can be figured out just by pattern matching/constraint propagation, then we are done. Otherwise, try all options. Recurse on the left half of the code and the right half of the code, propagating constraints as necessary. * On the difficulties of type annotation type-checking/type annotation is defintinely the most difficult part of my language. I now understand why people like extrinstic typing. * On Intrinsic typing Because I want my language to be intrinsically typed, a term can have multiple meanings depending on its type. For example, (empty : Int = 0), but (empty : Bool = false) and (empty : List = []) * Type Checking by pattern matching Here is a sample type signature for the annotation function #+BEGIN_SRC haskell annotateTerm : bindings -> rawTerm -> Maybe (bindings , rawTerm , type) #+END_SRC * Pattern Matching without names It seems that pattern matching without names is pretty difficult. For example, I think it would be easy to pattern match #+BEGIN_SRC haskell A -> A = Int -> Int #+END_SRC with the binding #+BEGIN_SRC haskell A = Int #+END_SRC But without names, it would be #+BEGIN_SRC joy type (dup ->) implicit-> = int int -> #+END_SRC Intuitiviely, we know the result should be [Int], but I'm not sure how an algorithm could figure this out. What about a case with restrictions? In haskell #+BEGIN_SRC haskell Monad m => m () = IO () #+END_SRC gives the binding m = IO if Monad IO. Without names, the same code would be: #+BEGIN_SRC joy // {m : Type -> Type} -> {_ : Monad m} -> m Unit type type -> (dup (Monad) dip (dropd Unit .) . implicit-> ) implicit-> = unit IO #+END_SRC This evaluates as #+BEGIN_SRC joy m dup (Monad) dip (dropd Unit .) . implicit-> = m m (Monad) dip (dropd Unit .) . implicit-> = m Monad m (dropd Unit .) . implicit-> = m Monad (m dropd Unit .) implicit-> => monadm m dropd Unit . = m Unit . = Unit m #+END_SRC * Pseudo-Code for type annotation here is some pseudo-code for the type annotation function in Javascript #+BEGIN_SRC javascript function annotateTerms(terms, expectedType){ } #+END_SRC