Wanted basic features - Githubissues

owo-lang / rfcs

RFCs: Feature requests, discussions, etc.

MIT License

3 stars 1 forks source link

Wanted basic features #2

Open ice1000 opened 5 years ago

ice1000 commented 5 years ago

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

ice1000 commented 5 years ago

Reflection (Agda, Idris)

ice1000 commented 5 years ago

Prop, Proof Irrelevance (Agda, Idris, Coq)

ice1000 commented 5 years ago

Sized Type (?) (Agda)

owo-lang/OwO#5 Redy!

ice1000 commented 5 years ago

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

ice1000 commented 5 years ago

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

ice1000 commented 5 years ago

Automatic Generalization (Haskell, Idris, OCaml)

ice1000 commented 5 years ago

Pattern Matching without K (Agda)

ice1000 commented 5 years ago

Overloading over lambdas (Agda)

Cubical Type Theories?

ice1000 commented 5 years ago

Foreign Function Interface (*)

ice1000 commented 5 years ago

Instance Arguments (Agda)

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

ice1000 commented 5 years ago

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

ice1000 commented 5 years ago

Global overloading (Idris)
Local shadowing (^Agda)

ice1000 commented 5 years ago

Metavariables (Haskell, Agda, Idris)

ice1000 commented 5 years ago

Universal Polymorphism (Agda, Idris, Coq)

anqurvanillapy commented 5 years ago

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 commented 5 years ago

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 commented 5 years ago

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

anqurvanillapy commented 5 years ago

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 commented 5 years ago

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 commented 5 years ago

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

ice1000 commented 5 years ago

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