#rust-lang

shep: are you trying to troll me lol

woboats: I'm not in love with `..=`, but (a) I want the feature and (b) you can blame Ruby's random number generator

Is that what we are talking about?

it is

I stood aside on ..= because the rest of the lang team was in consensus

I can reassign, if you'd like

It's just one more die roll

Well, actually

it picked you again

then...

it picked nrc

say the word

assign it to nrc

i want to at least be the last one to check my box which means I can't very well propose the merge

done <3

stick to those principles

eddyb: not sure what you meant by the syntax: 'Variant(A, B, C): Enum<T, U>' and how it enables things like data a :-> c where (:+:) :: (a :-> c) -> (b :-> c) -> (Either a b :-> c) ; ...'

centril: it's a syntactical transformation but your non-identifier names are very annoying

also the reuse of A and C

I'd use A and R

data PFun a c where Sum :: PFun a c -> PFun b c -> PFun (Either a b) c ..

centril: Sum<X, Y>(PFun<X, R>, PFun<Y, R>): PFun<Either<X, Y>, R>

Rust wouldn't let you reuse type parameter names like Haskell does

A = Either<X, Y>

eddyb: Sum is a variant I take it ?

yes

that'd be inside enum PFun<A, R>

centril: literally "the type of the constructor"

Ah, so you use <X, Y> for existential quantification of X & Y

yupp

just like Haskell

I mean

if it were a true existential it wouldn't be allowed

eddyb: yea with <X, Y> it becomes immediately obvious to me

here it's X = (A as Either).0 and Y = (A as Either).1 (in very pseudo notation)

eddyb: I assume you can also put bounds on X & Y like so: Sum<X: Copy, Y: Copy>(..): ..

If 'where' was involved I think it would come last, like so: Sum<X, Y>(PFun<X, R>, PFun<Y, R>): PFun<Either<X, Y>, R> where X: Copy, Y: Clone,

that gets trickier but sure

eddyb: so expand on "if it were a true existential"?

the problem is determining variant parameters from the actual enum parameters

they are not "arguments" but a logical variable shorthand for something that we have no syntax for

but we can do with custom traits

i.e. trait IsEither { type Left; type Right; const PROOF: Id<Self, Either<Self::Left, Self::Right>>; }

wait what

eternaleye: ^^ associated consts can encode proofs

compile-time dependent records

reminiscent of 1ML?

just not as general

eddyb: so I'm not sure I follow on the custom traits thing

hmm... could we express: data TypedExpr where (:::) :: forall t. Eq t => Expr t -> Type t -> TypedExpr ? Perhaps as: enum TypedExpr { TExpr<T: Eq>(Expr<T>, Type<T>), } ?

Hmm, reading over https://github.com/rust-lang/rfcs/blob/master/t...

it seems that adding an impl of a fundamental trait is breaking, but a non-fundamental is not,

so shouldn't Drop be a fundamental trait?

It doesn't seem to be: https://doc.rust-lang.org/src/core/ops/drop.rs....

but implementing it is certainly a breaking change, due to its impact on dropck.

centril: you can pattern-match on types with traits

furthermore, you can prove the types have a certain head!

eddyb: so in the TypedExpr example, I see a problem... We can construct a TypedExpr::TExpr::<ConcreteT>(expr, ty) with a known size, but given a TypedExpr, how could we possibly know the size of TypedExpr?

eddyb: I think I need to see things in a larger context to understand what you mean

centril: my example introduces no existentials/universals

it relies on type pattern-matching

just like in <Iter: Iterator<Item = (A, B)>, A, B> A and B are *not* truly universal

they are Iter::Item.0 and .1

projections

eddyb: interesting; but then TypedExpr would not work I take it?

centril: correct, you'd need a boxed trait object or something