Lambda the Ultimate

In the following (Haskell) example, the type annotation on f is required:

f :: a -> (Int, a)
f x = (g True, x)

g True = 0
g False = fst (f 'a') + fst (f 0)

main = do
    print (fst (f True))

I can understand why in general, but I wonder if we could just decide to generalize arbitrarily in the order that declarations appear so that in this case the type of f would be inferred but if you switched the definition order you'd get a type error. When f is generalized, g would be constrained Bool -> b where b would be unified after generalization. Is this something that might work (but isn't done because it's arbitrary and makes definition order matter) or are there hard cases I need to consider?

Thanks

Kitten has ad-hoc static polymorphism in the form of traits. You can declare a trait with a polymorphic type signature, then define instances with specialisations of that signature:

// Semigroup operation
trait + <T> (T, T -> T)

instance + (Int32, Int32 -> Int32) {
  _::kitten::add_int32
}

instance + (Int64, Int64 -> Int64) {
  …
}
…

This is checked with the standard “generic instance” subtyping relation, in which <T> (T, T -> T) ≤ Int32, Int32 -> Int32. But the current compiler assumes that specialisations are fully saturated: if it infers that a particular call to + has type Int32, Int32 -> Int32, then it emits a direct call to the (mangled) name of the instance. I’d like to remove that assumption and allow instances to be generic, that is, partially specialised:

// List concatenation
instance + <T> (List<T>, List<T> -> List<T>) {
  _::kitten::cat
}

// #1: Map union
instance + <K, V> (Map<K, V>, Map<K, V> -> Map<K, V>) {
  …
}

// #2: A more efficient implementation when the keys are strings
instance + <V> (Map<Text, V>, Map<Text, V> -> Map<Text, V>) {
  …
}

But this raises a problem: I want to select the most specific instance that matches a given inferred type. How exactly do you determine that?

That is, for Map<Text, Int32>, #1 and #2 are both valid, but #2 should be preferred because it’s more specific. There are also circumstances in which neither of two types is more specific: if we added an instance #3 for <K> (Map<K, Int32>, Map<K, Int32> -> Map<K, Int32>), then #2 and #3 would be equally good matches, so the programmer would have to resolve the ambiguity with a type signature.

Hi, I wonder if someone can help resolve the conflict described below.

My system is an Algol like language which supports both functional and procedural code.
Now, I hate the way C handles lvalues, it doesn't extend well, one has to make horrible rules
and list all possible l-contexts, and attempts to do this in C++ are an abysmal failure.
My solution is elegant! Consider a record:

(x=1,y=42.1)

which has type

(x:int, y:double)

then this is a first class value, and the field names are projections:

x (x=1,y=42.1)

Since I have overloading there's no conflict with the same field name in some other record,
the field name is just an overloaded function name.
To make it look nicer you can use reverse application:

(x=1,y=42.1) . x

Now, to get rid of lvalues we introduce pointer types and variables so that in

var xy = (x=1,y=42.1);
&xy <- (x=2,y=43.1);

This is really cool because & is not an operator,
just a way to write the value which is the address of a variable.
We use a procedure written as infix left arrow which takes a pointer to T
as the first argument and a T as the second, and stores the value at the specified address. So its all values.

To assign to a component, we introduce a second overload for each projection that takes a pointer argument and returns a pointer:

&xy . x <- 3;

This works for other products as well (tuples, arrays and structs).
So, we have a purely value based semantics and a sane type system.
In particular we have a very nice rule that relates values and objects.

So far so good, but now I have another feature called "compact linear types"
which are packed encodings of any type defined by the rule:
unit is compact linear, and sum, product, or exponential of a compact linear type is compact linear.
A small compact linear types is one that fits in a 64 bit machine word.
So for example the type 3 * 4 is a single 64 bit value which is a subrange of integer 0 thru 11.
Compact linear types with integer coercions used as array indices give polyadic arrays
(rank independent array programming).

The problem is .. compact linear type components are not addressable.
Projections functions work fine, but there are no overloads for pointer projections.

And so the conflict: polymorphic pointer projections are unsound:

proc f[T,U] (r: &(T,U)) (v:T)) { r.0 <-v; }

will not work if r is a pointer to a compact linear object. I can think of three solutions:

(1) invent a new pointer type (destroys uniform pointer representation property)
(2) have distinct product, sum, and exponential operators for compact linear types
(3) use the same operators but introduce pack and unpack operations

Writing computer games for people to play, even quite simple ones, is a surprisingly challenging task. Here I'm thinking of turn-based games like card and board games, puzzles, block-pushing and perhaps simple arcade games like Space Invaders. It would seem fairly obvious that large parts of the heavy lifting will be common from one to another and that differences in game play might well be encapsulated in a DSL.

Others have had the same thought. Here are links to some good reviews: https://chessprogramming.wikispaces.com/General+Game+Playing, https://en.wikipedia.org/wiki/Domain-specific_entertainment_language, https://en.wikipedia.org/wiki/General_game_playing. The GGP language GDL is a Datalog derivative, Zillions uses a Lisp dialect and Axiom is a kind of Forth. There are several others, including PuzzleScript, CGL and VGDL. GGP in particular is the focus of a lot of AI work, not so much the UI. Several of these projects appear dormant.

Considering the prevalence of games in the community and the number of people involved in writing them, this looks like surprisingly little effort in this direction. I was wondering if anyone is aware of or involved in any active work in this area, particularly on the language side, before I go and invent my own.

Monads are an awkward effects model in context of concurrency. We get incidental complexity in the form of futures or forking threads with shared memory. The running program becomes entangled with the environment, which hinders persistence and mobility and debugging. So I sought alternatives in literature.

Kahn Process Networks (KPNs) seem like a very good alternative. From an external perspective, they share a lot of similarities to monads, except we get more than one input (continuation) and output (effect) port and thus can model concurrent operations without relying on effects or environment support. Internally, KPNs have a lot of similarities to free monads: we can compose KPNs to handle effects internally, translate them, etc.. Use of KPNs as first class values allows for dynamic structure and mobile processes.

The main feature missing from KPNs is the ability to work with asynchronous inputs. But it is not difficult to add time to the model, and thus support asynchronous messaging and merges in a style similar to functional-reactive or flow-based programming (and somewhere between the two in terms of expressiveness). I doubt this is a new idea.

I've written about these ideas in more detail on my blog:

• KPNs as an Effects Model - a pure alternative to monads.
• Reactive Process Networks - add a simple time model to KPNs.

Reactive KPNs with open ports or channels also make a better FRP than most, having a far more direct API for pushing inputs and pulling outputs deep within a network.

Is it possible to create recursive function using monads in a functional language?

definition of monad in a functional language should look like: "a->(a->b)->b". Is it possible to have "a" as a parameter, get "b" as a result and recursively repeat it until some condition is satisfied? I've been strugling over factorial example, but I don't see a clear solution.

The reason I'm asking is that I'm defining a language where functions are passed around together with applied parameters. If I repeatedly call a function by a recursion, new data sums with previous data that was there before the recusion was applied. So finally I'd get a set of all intermediate results, while I'm interested only in the final result. I'm not even sure if monads would work in this environment with data stitched to function calls.

Actually, a solution I can use is first to create a set of parameters of each recursion step, and then to call some kind of fold function over the set that produces a single result. But I want to explore other possibilities, so I'm interested in monadic or other solutions.

Thank you for your time.

Does anyone have a reference to a correct algorithm which eliminates left recursion from a grammar? The one in Wikipedia is incorrect. Lots of youtube videos and lecture notes Google finds are also incorrect. All make the same mistake, they forget that a production A = N A X is left recursive if N is nullable. Requiring the grammar to be null free would be absurd since the algorithm itself inserts epsilon productions.

I also wish to extend the requirement to an attribute grammar of the form usually used in practice, with an extra symbol kind for AST construction, etc, which cannot be eliminated and yet recognises the empty string.

BTW: I'm looking for the basic algorithm. Lost my copy of the Dragon Book ;(

Hi,

I have an idea for an academic paper, and am seeking help for prior art and research.

My idea is about proof witnesses, and what to do when a group of witnesses contradict each other (software bug/logical inconsistency), and repairing the proof. Without going into details on the algorithm, the metaphor is simply to split witnesses up, using a mathematical plane to draw a group of witnesses into two groups: definitely lying (the witness whose account is proven contradictory/false), and somewhat certain (witnesses with similar testimonies who have not yet been proven contradictory/false, but might once asked further questions or may be proven "good enough" given the new questions/evidence we've asked the witness about). My idea comes from witness interrogation techniques in the real world.

Since I haven't been active in PLT for several years, my knowledge of what to search for and keywords to use on ACM and IEEE search engines is pretty weak, and I could use some tips.

Thank you very much!

I'm interested in libraries that guide compilers for optimizations, but it
seems like there isn't much literature on this topic.

- Papers like "Generative Programming and Active Libraries" which usually just
briefly talk about the idea and give the same examples like Blitz++.

- There's a thesis, "Active Libraries and Universal Languages", which as far as
I can see is a bit too light on the practical examples and implementation.

Two implementations that work well:

- I think Haskell libraries that use GHC's rewrite rules are "active libraries"
in this sense

- The stream fusion library described in POPL'17 paper "Stream Fusion, to
Completeness" is an example that's a recent work and one that works really
well (although it has problems like leaking `code` type to the user in
functional arguments).

These are pretty much all I can think of as examples. I'm looking for recent
developments and other practical examples (i.e. ones that work well and/or used
widely). Any pointers would be appreciated.

I’m working on a language and I would like to implement polymorphism over type constructors (for functor, applicative, monad, etc.) but I’m uncertain how to proceed.

Can anyone recommend tutorial-style resources or sample implementations of this? I’ve read that higher-order unification is involved, and that inference is undecidable without certain restrictions. Is that accurate? Would it be difficult to retrofit a (more or less) standard implementation of Hindley–Milner?