Wanted basic features

[ice1000]

No description provided.

[ice1000]

• GADT (Haskell, Agda, Idris) and Generalized Algebraic Codata Type (Agda)
• Dependent (Co)pattern matching (Agda)

[ice1000]

• Reflection (Agda, Idris)

[ice1000]

• Prop, Proof Irrelevance (Agda, Idris, Coq)

[ice1000]

• Sized Type (?) (Agda)

owo-lang/OwO#5 Redy!

[ice1000]

• Termination check, possibly cross function? (Agda, Idris, Coq)

[ice1000]

• Module System (Agda, OCaml)
  • import
  • open
  • open {{ ... }}
  • parameterization
  • hiding
  • using
  • renaming

[ice1000]

• Automatic Generalization (Haskell, Idris, OCaml)

[ice1000]

• Pattern Matching without K (Agda)

[ice1000]

• Overloading over lambdas (Agda)

Cubical Type Theories?

[ice1000]

• Foreign Function Interface (*)

[ice1000]

• Instance Arguments (Agda)

I don't want typeclass/type instance as language component.

[ice1000]

• Strict evaluation for data, Lazy evaluation for codata? (^)

[ice1000]

• Global overloading (Idris)
• Local shadowing (^Agda)

[ice1000]

• Metavariables (Haskell, Agda, Idris)

[ice1000]

• Universal Polymorphism (Agda, Idris, Coq)

[anqurvanillapy]

What about n-truncated types like HoTT-Agda's to introduce hProp/hSet, make identity types and homotopy equivalence equivalent, and axiom K a theorem for hSet.

[ice1000]

What about n-truncated types like HoTT-Agda's to introduce hProp/hSet, make identity types and homotopy equivalence equivalent, and axiom K a theorem for hSet.

It has already been covered as Prop and Proof Irrelevance

[ice1000]

• Types with boolean refinement (F*), may replace sized type?

[anqurvanillapy]

It's an urge to give a research about the ability of modeling HoTT by UTT, since the base standard library of OwO should start with things like in HoTT-Agda's n-truncated types, since then we can easily model h-props and h-sets by postulating different axioms, and even forget about UA when modelling all the groupoids.

[anqurvanillapy]

And I will leave a comment about the design of record-like stuff, since I think Agda's (co-)inductive records are weird to construct...

[ice1000]

Yes, forget about record constructors. We'll use copatterns to replace record constructors!

[ice1000]

After a little study about cutt, I'd say proof irrelevance is no longer useful when we have path types.