[avmich]

> Hazel is a live functional programming environment that is able to typecheck, manipulate, and even run incomplete programs, i.e. programs with holes. There are no meaningless editor states.

Suppose I have an assigned variable, which later I plan to use. When I'm about to use it, but not yet did, I have a hole. Suppose before filling the hole I've realized that the current type of the variable - and assigned value - is wrong, so I want to use the correct type.

Can hole-oriented programming help me with that change of mind? When we use a program, using a configuration file but also allowing command-line overrides of values, we assume last-time command-line overrides have precedence over values in the configuration file. Can we consider later-time use of variable with different type overriding the previous type, which now considered to be incorrect? Of should the language catch us making a type error here?

[pbiggar]

I work on Dark (https://darklang.com), which uses a similar concept about holes to Hazel. I've looked at Hazel but amn't totally familiar, so take this answer in that context.

In the first case, the hole has a type. I believe this type is inferred by the compiler/editor/type-checker, and I believe it will tell you if they type is wrong (in Dark, we'll tell you if the type is wrong, though we'll still let you put that variable in that hole to support the transition from one valid state to another).

In the configuration file example, you can't change the type: these are statically typed functional languages, and they don't permit "later-time" type changes.

[willtim]

> should the language catch us making a type error here?

With a statically typed language, the choice is up to you. Every statically typed language is just a "dynamically typed" language with the ability to statically assign types. For example, you can type the variable as an "Int" or for more runtime flexibility, a "Variant" (if using C++).

[avmich]

The question here is that a type inference can assign type to a hole but may get confused if user insists on an incompatible type.

int q // q is considered a hole of int type

q <- // but we're typing "hello" there

Practicalities ask for the situation to be considered a problem - not of incorrectly plugged hole (when into "int" place you're putting "string" value), but of incorrectly previously stated type (it's the original "int q" which is wrong, should have been "string q").