How to create open sum type?

Stream: general

[Locria Cyber]

Like open type in Koka, I want to have a sum type with branches across many files.

Should I do AnyOf [TypeA, TypeB, ...] or something else? How do i Elab a inductive type to see its possible branches?

[Niels Voss]

To confirm, you want an inductive type where you can dynamically extend the possible branches of the type after it has already been defined?

[Locria Cyber]

idk if it is "after it has already been defined".

Is it possible to put add_branch [...] anywhere in the source repository and have it scanned? There has been a few times during ordinary programming that I hoped the language had this feature.

[Niels Voss]

I'm not sure this is possible. The problem is that if you create an inductive type A, you can define a function A -> SomeOtherType by pattern matching on A. But if there were a way to add more branches to A, it would break all the functions that pattern matched on A. So it must be that if there were a way to define an open inductive or something, you wouldn't be able to pattern match on it.

The alternative would be to make A into a typeclass. Since you couldn't pattern match on A anyways, it seems this meets your requirements, and then you can dynamically extend it later with instance.

The inductive types vs typeclasses tradeoff is known as the Expression problem. It is effectively the same as the trade-off between normal classes/interfaces and sealed classes in Java.

[Locria Cyber]

But Type is not inductive.

TypeA.mk : Nat -> TypeA
TypeB.mk : String -> TypeB

If I use typeclass, the constructor parameter type is erased. How do I use elaboration to make a "sum type" constructor and eliminator?

[Niels Voss]

Can you maybe link to some documentation on what open type does in Koka? I couldn't find any documentation of it with a quick search.

[Locria Cyber]

https://github.com/koka-lang/koka/discussions/631
search for extend type

[Robin Arnez]

From the discussion you sent: https://koka-community.github.io/koka-docs/koka-docs.kk.html#sec-type-definitions

[Locria Cyber]

This is more of a convenience thing. Not about type theory.

[Robin Arnez]

You could use docs#Dynamic, which is basically "any type that has deriving TypeName"

[Locria Cyber]

The type of a parameter of a constructor of a branch may be defined later than the typeclass.

[Niels Voss]

The semantics of this are actually pretty complicated, so I'm not actually sure how this would be done. One complication I can imagine is that if you declare an open type A : Type and allow extending what values it can have in the future, then A must have cardinality larger than every type in Type, because for any B : Type you can extend A to allow values of B. This leads to a logical inconsistency. The alternative is to give A a universe bump or make it opaque-ish.

[Locria Cyber]

the compiler can prevent cycles

[Locria Cyber]

no paradox

[Locria Cyber]

it's one type with definitions split across many files

[Niels Voss]

At the very least, this means that if any definition x references A or something depending on A after it is defined, then when extending A with new branches those branches cannot depend on x. So the compiler would need to track dependencies for every open type for every definition.

[Niels Voss]

it's one type with definitions split across many files

Are you allowed to write theorems and definitions depending on the type between when the type is declared and when it is extended? If so, this is much more complicated than a standard inductive type

[Niels Voss]

I think with sufficient cleverness, something like this could be implemented without a universe bump by making an opaque type for which some properties can be proven, but the recursion principle is insufficiently powerful to ever allow establishing an upper bound on the type's cardinality. I don't think this would be a conservative extension of Lean.

[Niels Voss]

That is, you could have something like (and clearly this is not the most optimal way to do it nor does it cover all concerns)

-- Declare open inductive type with two branches
opaque Fruit
opaque Fruit.isApple : Fruit -> Bool
opaque Fruit.getAppleSize : (f : Fruit) -> (f.isApple = true) -> Float
opaque Fruit.mkApple : Float -> Fruit
axiom Fruit.isApple_mkApple (x : Float) : Fruit.isApple (Fruit.mkApple x) = true
axiom Fruit.getAppleSize_mkApple (x : Float) : Fruit.getAppleSize (Fruit.mkApple x) ... = x
opaque Fruit.isBanana : Fruit -> Bool
opaque Fruit.getBananaLength : (f : Fruit) -> (f.isBanana = true) -> Float
opaque Fruit.mkBanana : Float -> Fruit
axiom Fruit.isBanana_mkBanana (x : Float) : Fruit.isBanana (Fruit.mkBanana x) = true
axiom Fruit.getBananaLength_mkBanana (x : Float) : Fruit.getBananaLength (Fruit.mkBanana x) ... = x
axiom Fruit.not_isApple_mkBanana (x : Float) : Fruit.isApple (Fruit.mkBanana x) = false
axiom Fruit.not_isBanana_mkApple (x : Float) : Fruit.isBanana (Fruit.mkApple x) = false

and then later on you can extend it with a third branch:

opaque Fruit.isPersimmon : Fruit -> Bool
opaque Fruit.getPersimmonSpecies : (f : Fruit) -> (f.isPersimmon = true) -> String
opaque Fruit.mkPersimmon : String -> Fruit
axiom Fruit.isPersimmon_mkPersimmon (x : String) : Fruit.isPersimmon (Fruit.mkPersimmon x) = true
axiom Fruit.getPersimmonSpecies_mkPersimmon (x : String) : Fruit.getPersimmonSpecies (Fruit.mkPersimmon x) ... = x
axiom Fruit.not_isPersimmon_mkApple (x : Float) : Fruit.isPersimmon (Fruit.mkApple x) = false
axiom Fruit.not_isPersimmon_mkBanana (x : Float) : Fruit.isPersimmon (Fruit.mkBanana x) = false
axiom Fruit.not_isApple_mkPersimmon (x : String) : Fruit.isApple (Fruit.mkPersimmon x) = false
axiom Fruit.not_isBanana_mkPersimmon (x : String) : Fruit.isBanana (Fruit.mkPersimmon x) = false

[Niels Voss]

The point is, Fruit must always be under-specified, in the sense that at any point in the code there exist multiple non-isomorphic types that satisfy all the axioms of Fruit so far. And it is impossible to find a cardinal C and prove that the cardinality of Fruit is less than C. And for any cardinal C, we can extend Fruit such that it has cardinality greater than C. But this doesn't let us derive a contradiction.

[Kenny Lau]

it seems like @Locria Cyber might be happy with each new constructor being countable and there only being finitely many constructors

[Kenny Lau]

but then it also seems like we'll need some sort of metaprogramming to store what branches have been declared (as this is not static)

[Niels Voss]

I am a bit worried this breaks some important property of the logic though. I was thinking it might break omega-consistency, but now I'm not actually sure it does.

[Niels Voss]

Oh, and yeah, we are not allowed to extend Fruit to have a branch with elements of Set Fruit. But I think this should be covered when you write that you require each new branch to be countable.

[Locria Cyber]

It's not about the logic, but about code organization. Instead of defining a type in one file, now it's defined in many files.

[Aaron Liu]

do you just want an "extendable enum" or something more complicated

[Aaron Liu]

if it's just an enum without anything inside then you can just implement it as Nat

[Aaron Liu]

if it's something more complicated then it might be more tricky

[Aaron Liu]

but this also might be an #xy

[Locria Cyber]

if it's just an enum without anything inside then you can just implement it as Nat

How to have the compiler assign a number?

[Aaron Liu]

unfortunately you'll have to assign the numbers yourself

[Locria Cyber]

how to scan through the source code in a lake file?

[Aaron Liu]

since it has to work across the import graph without having collisions

[Aaron Liu]

Locria Cyber said:

how to scan through the source code in a lake file?

what do you mean by this?

[Aaron Liu]

what are you looking for in the scan

[Aaron Liu]

why is it coming from the lake file?

[Locria Cyber]

say, #[open_type] def ...

[Locria Cyber]

because it can only be done by a build tool

[Aaron Liu]

what does that mean

[Locria Cyber]

the build system generates the sum type definition from the rest of the source code

[Aaron Liu]

oh do you want a script that goes through the files and figures out an assignment of numbers for you

[Locria Cyber]

yes

[Aaron Liu]

well, what have you tried so far?

[Locria Cyber]

for other languages, opengrep

[Locria Cyber]

Go has go generate

[Aaron Liu]

I guess the other option would be to implement it as String and then you don't have to worry about the numbers anymore

[Locria Cyber]

it is exactly about functions with different signatures.

[Locria Cyber]

e.g. i want to register some Python extensions on load, in a type safe manner.

[Aaron Liu]

what do you mean "register"

[Aaron Liu]

and what are python extensions

[Locria Cyber]

C code that extends Python. They have to be registered before used in Python.

[Aaron Liu]

ok

[Locria Cyber]

Is there like a #[do_something] that is a no-op but appear in AST?

[Aaron Liu]

I don't think there's anything that's specifically for that purpose

[Aaron Liu]

but Lean has extensible syntax so you can just extend the syntax to have a noop

[Locria Cyber]

:+1:

[Anthony Wang]

Locria Cyber said:

Like open type in Koka, I want to have a sum type with branches across many files.

Should I do AnyOf [TypeA, TypeB, ...] or something else? How do i Elab a inductive type to see its possible branches?

Is this the same thing as polymorphic variants in OCaml?

[Mario Carneiro]

No one seems to have mentioned that Lake has an implementation of open types already via the family_def macro

[Yury G. Kudryashov]

https://lean-lang.org/doc/api/Lake/Util/Family.html