Closed LighghtEeloo closed 1 year ago
Sample syntax for forall
and exists
:
data Seal (X : VType) (A : VType) where
| Seal(Thunk(A -> Ret X), Thunk(X -> Ret A))
end
def id : Thunk(forall (A : VType) . A -> Ret A) = {
fn (A : VType) -> fn x -> ret x
} end
def nat : exists (X : VType) . Seal X Int = pack(
Int, Seal(
{ ! id @(Int) },
{ ! id @(Int) },
)
) end
match nat | pack(Nat, seal) ->
match seal
| Seal(of, to) ->
do n <- ! of 0;
do i <- ! to n;
! exit i
end
end
Though we've introduced for-all and exists types since e1918145c6efdd8e5cb7830be286b0e8b6bde7c3, they are a bit lengthy to use rn. It might be better to allow an implicit version of for-all typed terms optionally.
The only change I can smell of happens in the type checker. Since we are only checking type functions against for-all types, here's my proposal:
fn ->
for a better (?) code style.@maxsnew Would you kindly share your thoughts on whether this solution appears to be feasible?
As discussed in the weekly meeting, with the successful implementation and integration of the explicit version of System-F, we are now in a good position to close this issue.
As a next step, a separate issue will be opened to address the implementation of implicit polymorphism. This new issue will focus on enhancing the language's expressiveness and user experience, leveraging the strong foundation laid by the explicit System-F implementation.
At this stage we should consider bringing system-F to our language. Due to the fact that we are dealing with CBPV, we've decided to make for-all types computation types and exists types value types.
Sample syntax: