Stream: t-compiler

Topic: const generics in const fn


Bastian Kauschke (Apr 13 2020 at 19:16, on Zulip):

We currently forbid const generics in const fn:

#![feature(const_generics)]

const fn foo<const N: u32>() -> u32 {
    //~^ ERROR const parameters are not permitted in const functions
    N + 1
}

This rationale for this is explain in the doc comment for fn AstValidator::check_const_fn_const_generic:

We currently do not permit const generics in const fn, as this is tantamount to allowing compile-time dependent typing.

FIXME(const_generics): Is this really true / necessary? Discuss with @varkor. At any rate, the restriction feels too syntactic. Consider moving it to e.g. typeck.

We can use the const param of an impl to circumvent this.

#![feature(const_generics)]

struct Indirect<const N: u32>;

impl<const N: u32> Indirect<N> {
    const fn foo() -> u32 {
        N + 1
    }
}

fn main() {
    println!("{}", Indirect::<7>::foo());
}

Is there a case where foo::<value>() can be used while Indirect::<value>::foo() is unusable?
@varkor cc @eddyb

eddyb (Apr 13 2020 at 19:18, on Zulip):

that comment doesn't make sense to me

eddyb (Apr 13 2020 at 19:18, on Zulip):

you should be able to just remove the restriction

eddyb (Apr 13 2020 at 19:18, on Zulip):

I had no idea we had it

eddyb (Apr 13 2020 at 19:18, on Zulip):

also btw you need 0 const fn to compute consts from other consts

eddyb (Apr 13 2020 at 19:19, on Zulip):
#![feature(const_generics)]

struct Indirect<const N: u32>;

impl<const N: u32> Indirect<N> {
    const FOO: u32 = N + 1;
}

fn main() {
    println!("{}", Indirect::<7>::FOO);
}
eddyb (Apr 13 2020 at 19:19, on Zulip):

this just works :P

eddyb (Apr 13 2020 at 19:19, on Zulip):

(or I assume it does, I haven't tried it)

Bastian Kauschke (Apr 13 2020 at 19:21, on Zulip):

Will try and go ahead with removing it them. git blame points to @centril

Bastian Kauschke (Apr 13 2020 at 19:23, on Zulip):

this just works :P https://play.rust-lang.org/?version=nightly&mode=debug&edition=2018&gist=532a4d3d70bf6a5630175384a3c2d3a9

(I know it does, I have tried it)
:heart:

centril (Apr 13 2020 at 19:58, on Zulip):

I also think we can just remove the restriction

Bastian Kauschke (Apr 13 2020 at 20:38, on Zulip):

https://github.com/rust-lang/rust/pull/71109

varkor (Apr 13 2020 at 20:55, on Zulip):

allowing const generics on const fn was deliberately not permitted for the initial version of const generics, cc @boats

varkor (Apr 13 2020 at 20:58, on Zulip):

it may be safe to allow at some point, but it's not trivially safe, so we ought not to be so cavalier about it

varkor (Apr 13 2020 at 20:59, on Zulip):

naïvely, a const function with a const generic parameter is a function whose type depends on a value in the same stage of compilation as it is executed, i.e. a dependent function

varkor (Apr 13 2020 at 21:00, on Zulip):

I may have had a specific example I was concerned about, but I would have to think about it/try to find it

varkor (Apr 13 2020 at 21:00, on Zulip):

at the very least, this is certainly a decision question — not something to accidentally permit without thinking through the consequences

varkor (Apr 13 2020 at 21:02, on Zulip):

it may be that as long as we push the obligations to the callers to verify correctness, as with @eddyb's WF bounds for consts, that this is okay — but even the WF bounds are an open design question at the moment

eddyb (Apr 13 2020 at 21:03, on Zulip):

I don't understand what you're saying

eddyb (Apr 13 2020 at 21:03, on Zulip):

how is this more dependent typing than anything else?

eddyb (Apr 13 2020 at 21:03, on Zulip):

did you see the examples that use only associated consts?

eddyb (Apr 13 2020 at 21:03, on Zulip):

in facts, by replacing const generics with types that implement a trait with associated consts, you can make examples that compile on stable

eddyb (Apr 13 2020 at 21:04, on Zulip):

I don't understand the argument: the type of the function is not special at all, it's just another struct

eddyb (Apr 13 2020 at 21:05, on Zulip):

there may be some confusion with higher-ranked things?

eddyb (Apr 13 2020 at 21:05, on Zulip):

but we don't have for<const N: usize> or w/e yet, so that's not a concern

eddyb (Apr 13 2020 at 21:06, on Zulip):

@varkor okay so trying to understand this, is the concern that an argument of a const fn may be used in a type?

eddyb (Apr 13 2020 at 21:06, on Zulip):

e.g. const fn(n: usize) -> [T; n]?

eddyb (Apr 13 2020 at 21:07, on Zulip):

because 1. this is impossible today 2. this is impossible in general without full dependent typing, because const fns are just fns you can also call at compile-time

eddyb (Apr 13 2020 at 21:07, on Zulip):

they still have to work with runtime values

eddyb (Apr 13 2020 at 21:08, on Zulip):

@varkor dependent typing doesn't have anything to do with "stages of compilation", that's something else entirely

eddyb (Apr 13 2020 at 21:09, on Zulip):

it's all about universes

eddyb (Apr 13 2020 at 21:09, on Zulip):

or kinds, in Haskell terms

eddyb (Apr 13 2020 at 21:11, on Zulip):

dependent typing at compile-time would be this:

const FOO: &[u8] =  &{
    let n = 3;
    [0; n]
};
eddyb (Apr 13 2020 at 21:11, on Zulip):

and this is not something we allow or could allow any time soon

varkor (Apr 13 2020 at 21:11, on Zulip):

sorry, I'll think about this soon

eddyb (Apr 13 2020 at 21:13, on Zulip):

any type-level constants must come from separate compile-time evaluation. the separation is the important part, the compile-time is just because we're type-checking while compiling and the separation imposes a "happens before" relationship

eddyb (Apr 13 2020 at 21:13, on Zulip):

and the separation can be modeled as lifting to kinds

eddyb (Apr 13 2020 at 21:14, on Zulip):

const N: T becomes N: ConstValue<T>

eddyb (Apr 13 2020 at 21:14, on Zulip):

using N becomes N::VALUE

eddyb (Apr 13 2020 at 21:15, on Zulip):

(Haskell can use kinds for this, we can only mess around with traits :P)

eddyb (Apr 13 2020 at 21:16, on Zulip):

wow I got really worked up about dependent typing huh

eddyb (Apr 13 2020 at 21:17, on Zulip):

I guess seeing that explanation broke my brain a bit the second time since the first time I thought it was some confusion

eddyb (Apr 13 2020 at 21:18, on Zulip):

or misunderstanding

varkor (Apr 13 2020 at 21:22, on Zulip):

I admit: I had a knee-jerk reaction because I remember having a worry about this setting; but I need to think about what exactly the issue was — I thought it was better to delay bors for an hour or two than to have to back a change out because something was actually unsound

varkor (Apr 13 2020 at 21:22, on Zulip):

it could well be that the case I was worried about is not possible without interacting with another feature we don't have

varkor (Apr 13 2020 at 21:23, on Zulip):

but I'm in the middle of something at the moment, so it'll take me a little while to concentrate on this

eddyb (Apr 13 2020 at 21:25, on Zulip):

yeah no worries

eddyb (Apr 13 2020 at 21:26, on Zulip):

I'm happy with delaying until we can figure out how that reasoning came to be

eddyb (Apr 13 2020 at 21:26, on Zulip):

it just struck me as not meaning anything. if anything, any restriction should be for the benefit of min_const_fn (which bans e.g. trait bounds), not const generics

varkor (Apr 13 2020 at 21:29, on Zulip):

I imagine the rationale was that const fn foo<const X: usize>() -> [(); X] corresponds to something like x:usizeArray(x)\prod_{x : \mathrm{usize}} \mathrm{Array}(x)

centril (Apr 13 2020 at 21:48, on Zulip):

@varkor well it does, but of course there's a compile time restriction on the usize there

centril (Apr 13 2020 at 21:49, on Zulip):

I thought when we last discussed this in private that there was no problem

eddyb (Apr 13 2020 at 21:49, on Zulip):

@varkor except you can write that without const fn

varkor (Apr 13 2020 at 21:49, on Zulip):

I don't remember; everything is so out of cache, I need to try to reconstruct it to make sure my worries are unfounded

eddyb (Apr 13 2020 at 21:49, on Zulip):

that's just an associated const

centril (Apr 13 2020 at 21:49, on Zulip):

At any rate, the syntactic condition in AST validation is insufficient -- it does not consider impls and whatnot -- if you actually want to enforce this you should move it to rustc_typeck

varkor (Apr 13 2020 at 21:50, on Zulip):

@eddyb: right, that's what I'm currently thinking about

eddyb (Apr 13 2020 at 21:50, on Zulip):

there's no actual \Pi, since that would work with any values

centril (Apr 13 2020 at 21:50, on Zulip):

(well I suppose you can enforce it in AST validation as well, but you'll need a more elaborate check)

eddyb (Apr 13 2020 at 21:50, on Zulip):

it's more like x: const usize

eddyb (Apr 13 2020 at 21:51, on Zulip):

where const usize is an universe/kind of lifted values of type usize

centril (Apr 13 2020 at 21:51, on Zulip):

I think the Haskell analogue of const generics is {-# LANGUAGE DataKinds #-}

eddyb (Apr 13 2020 at 21:51, on Zulip):

yupp

eddyb (Apr 13 2020 at 21:51, on Zulip):

that's what I'm referring to

centril (Apr 13 2020 at 21:51, on Zulip):

Yeah :slight_smile:

eddyb (Apr 13 2020 at 21:52, on Zulip):

I just always forget they're data kinds since I think of this as "const kinds" :P

eddyb (Apr 13 2020 at 21:52, on Zulip):

anyway you can lift every value to type-encoded ADTs

eddyb (Apr 13 2020 at 21:52, on Zulip):

basically what typenum does but formalized

eddyb (Apr 13 2020 at 21:53, on Zulip):

this is why we need structurally matcheable ADT constructor trees with integer leaves

eddyb (Apr 13 2020 at 21:53, on Zulip):

and integers are only allowable because of the Nat ADT :P

centril (Apr 13 2020 at 21:55, on Zulip):

What we have is basically a new kind constructor Const : Type_Const -> Kind

centril (Apr 13 2020 at 21:55, on Zulip):

where _Const denotes the lifting

varkor (Apr 13 2020 at 22:08, on Zulip):

I suppose something like this is what I had previously been thinking of:

const fn bar(x: usize) -> usize {
    x
}

const fn foo<const X: usize>() -> [(); X] {
    [(); bar(X)]
}

sorry, my mind is somewhere else right now, so I'm not thinking entirely clearly

varkor (Apr 13 2020 at 22:09, on Zulip):

what is currently preventing this code from compiling if the const generics in const fn check is removed?

eddyb (Apr 13 2020 at 22:10, on Zulip):

that looks like correct code to me, I don't know what you mean

eddyb (Apr 13 2020 at 22:11, on Zulip):

this is entirely possible in an associated const

eddyb (Apr 13 2020 at 22:11, on Zulip):

bar(X) is not at the value level of foo

eddyb (Apr 13 2020 at 22:11, on Zulip):

it's lifted

centril (Apr 13 2020 at 22:11, on Zulip):

@varkor https://play.rust-lang.org/?version=nightly&mode=debug&edition=2018&gist=ed8aaace308dec4475c1b46d5337cd99

eddyb (Apr 13 2020 at 22:12, on Zulip):

oh lmao

centril (Apr 13 2020 at 22:12, on Zulip):
error[E0308]: mismatched types
  --> src/lib.rs:11:9
   |
10 |     const fn foo() -> [(); X] {
   |                       ------- expected `[(); _]` because of return type
11 |         [(); bar(X)]
   |         ^^^^^^^^^^^^ expected `X`, found `bar(X)`
   |
   = note: expected array `[(); _]`
              found array `[(); _]`
eddyb (Apr 13 2020 at 22:12, on Zulip):

right, we don't simplify bar(X) to X

centril (Apr 13 2020 at 22:12, on Zulip):

@varkor so as you see, the current check isn't actually enforcing anything :slight_smile:

eddyb (Apr 13 2020 at 22:13, on Zulip):

https://play.rust-lang.org/?version=nightly&mode=debug&edition=2018&gist=33b2deb1b5946d98d8f204e9882d3626

varkor (Apr 13 2020 at 22:14, on Zulip):

okay, let's leave aside that the current check is flawed: obviously that's a bug with the check, unrelated to the intention

eddyb (Apr 13 2020 at 22:14, on Zulip):

not only are const fns w/o arguments isomorphic to associated consts with #[feature(const_fn)], they're actually more restricted thanks to min_const_fn :P

eddyb (Apr 13 2020 at 22:14, on Zulip):

I don't know why you'd even bother with const fns when associated consts exist

varkor (Apr 13 2020 at 22:14, on Zulip):

eddyb said:

right, we don't simplify bar(X) to X

right, but this is a restriction with const generics at the moment

eddyb (Apr 13 2020 at 22:14, on Zulip):

surely if there is a problem in having const-generic constants, that would be it?

varkor (Apr 13 2020 at 22:14, on Zulip):

we don't always intend to have a completely syntactic check

varkor (Apr 13 2020 at 22:15, on Zulip):

eddyb said:

surely if there is a problem in having const-generic constants, that would be it?

I could believe that we're too liberal with associated constants and const generics at the moment

centril (Apr 13 2020 at 22:15, on Zulip):

eddyb said:

I don't know why you'd even bother with const fns when associated consts exist

Convenience and code reuse?

eddyb (Apr 13 2020 at 22:15, on Zulip):

no, I mean the checks needed from @varkor's PoV

eddyb (Apr 13 2020 at 22:16, on Zulip):

why would you bother banning const generics in scope of const fns when they can also exist in scope of associated consts

varkor (Apr 13 2020 at 22:16, on Zulip):

yeah, I agree

varkor (Apr 13 2020 at 22:16, on Zulip):

I think maybe we should ban const generics in associated constants

eddyb (Apr 13 2020 at 22:17, on Zulip):

okay now you have to convince me there is a reason to :)

varkor (Apr 13 2020 at 22:17, on Zulip):

okay, so I don't think there is any fear of this causing unsoundness

eddyb (Apr 13 2020 at 22:18, on Zulip):

I was worried you had something complicated involving arguments but if you think this restriction is needed by associated consts, I think I can safely say I believe you're mistaken :P

varkor (Apr 13 2020 at 22:18, on Zulip):

this is a safe underapproximation

varkor (Apr 13 2020 at 22:18, on Zulip):

but if we ever lift the syntactic restriction, i.e. the two terms must be identical, then we have issues with type checking

varkor (Apr 13 2020 at 22:18, on Zulip):

we have to rely on a limited form of symbolic execution

eddyb (Apr 13 2020 at 22:18, on Zulip):

this is fine with me even if bar(X) normalizes to X

eddyb (Apr 13 2020 at 22:19, on Zulip):

how so?

eddyb (Apr 13 2020 at 22:19, on Zulip):

bar(X) is not part of the parent body

varkor (Apr 13 2020 at 22:19, on Zulip):

because imagine bar is more complicated than the identity

varkor (Apr 13 2020 at 22:19, on Zulip):

it's some arbitrary function

eddyb (Apr 13 2020 at 22:19, on Zulip):

let x = bar(X); [(); x] will never work

varkor (Apr 13 2020 at 22:19, on Zulip):

we can't work out what it will return

varkor (Apr 13 2020 at 22:19, on Zulip):

are you saying [(); bar(X)] will never work?

eddyb (Apr 13 2020 at 22:19, on Zulip):

no

varkor (Apr 13 2020 at 22:19, on Zulip):

right

varkor (Apr 13 2020 at 22:20, on Zulip):

okay, I suppose this issue already exists, because we can have arbitrary expressions in the repeat parameter

eddyb (Apr 13 2020 at 22:20, on Zulip):

if it starts working, it will work all the same whether const fn or regular fn

eddyb (Apr 13 2020 at 22:20, on Zulip):

there is nothing about "this code may execute at compile-time" that changes any of this

eddyb (Apr 13 2020 at 22:21, on Zulip):

if unify(bar(X), X) will ever work it will be something mostly-syntactic on MIR most likely

eddyb (Apr 13 2020 at 22:21, on Zulip):

symbolic evaluation is hard :P

varkor (Apr 13 2020 at 22:21, on Zulip):

maybe…

centril (Apr 13 2020 at 22:21, on Zulip):

@eddyb we'd need to RFC some sort of definitional equality or so

centril (Apr 13 2020 at 22:21, on Zulip):

for "mostly syntactic on MIR"

eddyb (Apr 13 2020 at 22:22, on Zulip):

yeah sure, my point is

eddyb (Apr 13 2020 at 22:22, on Zulip):

none of this has anything to do with const fns or associated consts

centril (Apr 13 2020 at 22:22, on Zulip):

I agree with your point :slight_smile:

eddyb (Apr 13 2020 at 22:22, on Zulip):

I thought you were talking as if bar(X) is part of the parent body

eddyb (Apr 13 2020 at 22:22, on Zulip):

otherwise none of this "dependent typing" talk makes any sense

varkor (Apr 13 2020 at 22:22, on Zulip):

I think that my main issue was that type-checking could become (even more) undecidable, but I think this boils down to unify(bar(X), X), as you say, which was already an existing issue already

eddyb (Apr 13 2020 at 22:22, on Zulip):

let x = bar(X); [(); x] is dependent typing

eddyb (Apr 13 2020 at 22:23, on Zulip):

@varkor but you can just remove the const from the const fn and now it's not a const fn

centril (Apr 13 2020 at 22:23, on Zulip):

@varkor what does "even more undecidable" mean lol? :D

eddyb (Apr 13 2020 at 22:23, on Zulip):

and nothing changes about type-checking it

varkor (Apr 13 2020 at 22:23, on Zulip):

[(); { expression }] is dependent typing

eddyb (Apr 13 2020 at 22:23, on Zulip):

ah that's where your confusion stems from

eddyb (Apr 13 2020 at 22:23, on Zulip):

it's only if expression can refer to non-generics

centril (Apr 13 2020 at 22:24, on Zulip):

I think "dependent typing" isn't one thing; you can have degrees of dependent typing...

eddyb (Apr 13 2020 at 22:24, on Zulip):

but it can't

varkor (Apr 13 2020 at 22:24, on Zulip):

centril said:

varkor what does "even more undecidable" mean lol? :D

I thought you would correct me if I said "make it undecidable", as it already is

eddyb (Apr 13 2020 at 22:24, on Zulip):

that's why I'm saying let x = bar(X); [(); x] and [(); bar(X)] are very different

eddyb (Apr 13 2020 at 22:24, on Zulip):

the former is dependent-typing, no matter when let x may be evaluated

centril (Apr 13 2020 at 22:25, on Zulip):

And Haskell via DataKinds certainly have some sorta dependent typing; https://www.youtube.com/watch?v=wNa3MMbhwS4

eddyb (Apr 13 2020 at 22:25, on Zulip):

the latter is just data kinds

varkor (Apr 13 2020 at 22:25, on Zulip):

eddyb said:

it's only if expression can refer to non-generics

the generics can be arbitrary values, which means the type depends on some computation, whose value is not known without running some arbitrary code

eddyb (Apr 13 2020 at 22:25, on Zulip):

@varkor but you can lift all of that to types

varkor (Apr 13 2020 at 22:25, on Zulip):

eddyb said:

that's why I'm saying let x = bar(X); [(); x] and [(); bar(X)] are very different

I agree they are, and the former is much worse — but to some extend the latter is still dependent

eddyb (Apr 13 2020 at 22:25, on Zulip):

if you couldn't, then it would be dependent

eddyb (Apr 13 2020 at 22:25, on Zulip):

it's very important to understand where the value-level boundary lies

eddyb (Apr 13 2020 at 22:26, on Zulip):

X is not in the value level!

varkor (Apr 13 2020 at 22:26, on Zulip):

I understand your distinction

eddyb (Apr 13 2020 at 22:26, on Zulip):

okay then you should understand there is no concern here :P

eddyb (Apr 13 2020 at 22:26, on Zulip):

and no dependent typing

varkor (Apr 13 2020 at 22:26, on Zulip):

and I realise that it makes a practical difference

eddyb (Apr 13 2020 at 22:26, on Zulip):

there is a theoretical name for what const generics are but I've forgotten it

varkor (Apr 13 2020 at 22:26, on Zulip):

but now I'm just thinking about the terminological difference :P

eddyb (Apr 13 2020 at 22:26, on Zulip):

brb bugging eternaleye about it

centril (Apr 13 2020 at 22:26, on Zulip):

varkor said:

centril said:

varkor what does "even more undecidable" mean lol? :D

I thought you would correct me if I said "make it undecidable", as it already is

Just thought it a bit funny in the sense of "infinity + 1"

varkor (Apr 13 2020 at 22:27, on Zulip):

:P

varkor (Apr 13 2020 at 22:27, on Zulip):

"add more ways for it to be undecidable"

eddyb (Apr 13 2020 at 22:27, on Zulip):

inb4 this becomes ordinals vs cardinals

centril (Apr 13 2020 at 22:27, on Zulip):

@varkor maybe "more conveniently undecidable" ;)

centril (Apr 13 2020 at 22:29, on Zulip):

"In this release of Rust, we have made undecidability at the type level more accessible to all users"

eddyb (Apr 13 2020 at 22:29, on Zulip):

also I don't think MIR-driven unification is undecidable, only CTFE is

eddyb (Apr 13 2020 at 22:29, on Zulip):

my only interest in MIR-driven unification is treating two constant expressions written and type-checked the same, but in two different places, like they're equal

eddyb (Apr 13 2020 at 22:30, on Zulip):

okay, eternaleye replied

varkor (Apr 13 2020 at 22:30, on Zulip):

eddyb said:

my only interest in MIR-driven unification is treating two constant expressions written and type-checked the same, but in two different places, like they're equal

I personally would quite like symbolic execution, but I can see that that's a more contentious issue

eddyb (Apr 13 2020 at 22:30, on Zulip):

we can start simple shrug

eddyb (Apr 13 2020 at 22:32, on Zulip):

oh god now I can't find it

eddyb (Apr 13 2020 at 22:33, on Zulip):

no I don't want spirituality results

eddyb (Apr 13 2020 at 22:35, on Zulip):

awww apparently it's only in talks

varkor (Apr 13 2020 at 22:36, on Zulip):

eddyb said:

no I don't want spirituality results

what? :P

eddyb (Apr 13 2020 at 22:37, on Zulip):

something about having contacts in the spirit world

centril (Apr 13 2020 at 22:38, on Zulip):

@eddyb are we talking McBride's spirit world?

eddyb (Apr 13 2020 at 22:38, on Zulip):

anyway https://personal.cis.strath.ac.uk/conor.mcbride/pub/hasochism.pdf is kind of interesting

eddyb (Apr 13 2020 at 22:39, on Zulip):

@centril oh yeah I haven't said his name yet

varkor (Apr 13 2020 at 22:39, on Zulip):

eddyb said:

something about having contacts in the spirit world

I never thought spirits would be relevant to Rust :P

eddyb (Apr 13 2020 at 22:40, on Zulip):

it's how McBride refers to the kind of lifting here, apparently

eddyb (Apr 13 2020 at 22:40, on Zulip):

I was just hoping for something easier to point at, like a blog post or paper :P

varkor (Apr 13 2020 at 22:40, on Zulip):

I see :P

eddyb (Apr 13 2020 at 22:41, on Zulip):

sigh

eddyb (Apr 13 2020 at 22:42, on Zulip):

@varkor actually, I just got a flashback

eddyb (Apr 13 2020 at 22:42, on Zulip):

were you maybe concerned about calling const fns in AnonConsts used in types?

eddyb (Apr 13 2020 at 22:43, on Zulip):

as this would make more sense overall IMO

eddyb (Apr 13 2020 at 22:43, on Zulip):

even regular const fn, not necessarily ones parameterized by const generics, even completely monomorphic

eddyb (Apr 13 2020 at 22:43, on Zulip):

was surprised to see you bring up const unification but this would explain it

eddyb (Apr 13 2020 at 22:44, on Zulip):

this is not an unreasonable way to limit const unification, if we had it :P

centril (Apr 13 2020 at 22:44, on Zulip):

@eddyb that is something like TypeCtor<{foo::<Val>()}>?

eddyb (Apr 13 2020 at 22:45, on Zulip):

even TypeCtor<{const_fn(V)}>, assuming V is a const param

centril (Apr 13 2020 at 22:45, on Zulip):

don't have those (outside of the intrinsics), and doesn't matter?

eddyb (Apr 13 2020 at 22:45, on Zulip):

don't have what?

centril (Apr 13 2020 at 22:46, on Zulip):

non-implied const params

eddyb (Apr 13 2020 at 22:46, on Zulip):

I'm talking about literally Array<T, {add(N, 1)}>

eddyb (Apr 13 2020 at 22:46, on Zulip):

being disallowed but Array<T, {N+1}> allowed

centril (Apr 13 2020 at 22:46, on Zulip):

oh

eddyb (Apr 13 2020 at 22:47, on Zulip):

this is the only way I can understand @varkor's protests wrt the bar(X) example

eddyb (Apr 13 2020 at 22:47, on Zulip):

since clearly where that array shows up is unimportant: type-check works the same way

varkor (Apr 13 2020 at 22:47, on Zulip):

eddyb said:

were you maybe concerned about calling const fns in AnonConsts used in types?

yes

eddyb (Apr 13 2020 at 22:47, on Zulip):

/me gives out a sigh of relief

varkor (Apr 13 2020 at 22:48, on Zulip):

oh, actually, you're right: it is of course different to consider functions rather than expressions

eddyb (Apr 13 2020 at 22:48, on Zulip):

and yeah right now such expressions are quite useless so they're implicitly banned anyway :P

varkor (Apr 13 2020 at 22:48, on Zulip):

sorry, my sleeping schedule has gone out the window recently, and my mind obviously hasn't benefited from that :P

centril (Apr 13 2020 at 22:48, on Zulip):

@eddyb but what does add(N, 1) here have to do with the check in AST validation?

eddyb (Apr 13 2020 at 22:48, on Zulip):

nothing!

eddyb (Apr 13 2020 at 22:48, on Zulip):

that check is still confused IMO

eddyb (Apr 13 2020 at 22:49, on Zulip):

but I just found the link between const fns and const generics :P

centril (Apr 13 2020 at 22:49, on Zulip):

right; so we should nix it

eddyb (Apr 13 2020 at 22:49, on Zulip):

@varkor same and I've been meaning to sleep even before all of this kept me awake :P

varkor (Apr 13 2020 at 22:49, on Zulip):

eddyb said:

this is not an unreasonable way to limit const unification, if we had it :P

right, I think you've managed to decipher my incoherent thought patterns, thank you :sweat_smile:

varkor (Apr 13 2020 at 22:50, on Zulip):

eddyb said:

that check is still confused IMO

I'm pretty sure it was added as an afterthought, so this doesn't surprise me

centril (Apr 13 2020 at 22:53, on Zulip):

@eddyb not sure why we would disallow add(N, 1) though

eddyb (Apr 13 2020 at 22:53, on Zulip):

varkor said:

eddyb said:

this is not an unreasonable way to limit const unification, if we had it :P

right, I think you've managed to decipher my incoherent thought patterns, thank you :sweat_smile:

it literally came to me in a flashback so maybe I remembered a previous discussion

eddyb (Apr 13 2020 at 22:54, on Zulip):

@centril only once we get const unification, and maybe we won't ban it

centril (Apr 13 2020 at 22:55, on Zulip):

you'd need to expose the body of the const fn to look inside it if you e.g., want to unify add(N, 1) ~ add(1, N)

centril (Apr 13 2020 at 22:56, on Zulip):

@varkor so our conclusion is to r+ the PR again?

eddyb (Apr 13 2020 at 22:56, on Zulip):

btw add(1, 3) is clearly fine, it's only the "dependence" on const parameters that's dubious :P

centril (Apr 13 2020 at 22:57, on Zulip):

yeah

centril (Apr 13 2020 at 22:57, on Zulip):

@eddyb btw, "const parameters" is highly ambiguous :P

eddyb (Apr 13 2020 at 22:57, on Zulip):

how so?

eddyb (Apr 13 2020 at 22:57, on Zulip):

I use backticks to mean const X: T

centril (Apr 13 2020 at 22:57, on Zulip):

I would call it "const arguments"

centril (Apr 13 2020 at 22:58, on Zulip):

its the argument that is a constant; not the parameter?

eddyb (Apr 13 2020 at 22:58, on Zulip):

but that's not in the definition

eddyb (Apr 13 2020 at 22:58, on Zulip):

uhhhhh

eddyb (Apr 13 2020 at 22:58, on Zulip):

I mean generic parameters declared with the keyword const

eddyb (Apr 13 2020 at 22:58, on Zulip):

I wouldn't use this style if I meant "const" more informally

centril (Apr 13 2020 at 22:58, on Zulip):

@eddyb oh, fn foo(const N: usize)?

eddyb (Apr 13 2020 at 22:59, on Zulip):

no

eddyb (Apr 13 2020 at 22:59, on Zulip):

fn foo<const N: usize>

eddyb (Apr 13 2020 at 22:59, on Zulip):

or struct Foo<const N: usize>;

centril (Apr 13 2020 at 22:59, on Zulip):

oh; dependence on const parameters... never mind me

varkor (Apr 13 2020 at 23:04, on Zulip):

centril said:

varkor so our conclusion is to r+ the PR again?

yes, I think this is fine
we should record a note about const unification and calling const functions somewhere — do we have anywhere we're tracking comments about unification yet?

eddyb (Apr 13 2020 at 23:05, on Zulip):

there was a lot of discussion on the tracking issue that's probably lost now :(

eddyb (Apr 13 2020 at 23:05, on Zulip):

including some of my ideas

eddyb (Apr 13 2020 at 23:05, on Zulip):

well, "lost" unless you dare to press the "show 9000 comments" button

eddyb (Apr 13 2020 at 23:09, on Zulip):

anyway I don't think we have to ban it directly, we can just handle it by unification limitations

eddyb (Apr 13 2020 at 23:10, on Zulip):

the WF conditions we're adding will require that you somehow request that someone else evaluate it

eddyb (Apr 13 2020 at 23:10, on Zulip):

and unification won't work except in the identity case (but we have to be careful with Unevaluated unification)

varkor (Apr 13 2020 at 23:10, on Zulip):

yeah, I think these two facts protect us from anything unsavoury

eddyb (Apr 13 2020 at 23:19, on Zulip):

@varkor @centril https://www.youtube.com/watch?v=21bUrFEX4jI&t=1h2m30s

centril (Apr 13 2020 at 23:20, on Zulip):

I think I've seen this lecture at some point

eddyb (Apr 13 2020 at 23:21, on Zulip):

adjusted timestamp

eddyb (Apr 13 2020 at 23:28, on Zulip):

also wow, I am being informed GHC went an interesting route

eddyb (Apr 13 2020 at 23:28, on Zulip):
eddyb (Apr 13 2020 at 23:28, on Zulip):

<eternaleye> So yeah, GHC 7 had spirit mediums, but GHC 8 decided that we've all been dead all along

centril (Apr 13 2020 at 23:32, on Zulip):

@eddyb yeah, TypeInType is part of the move towards Dependent Haskell

centril (Apr 13 2020 at 23:32, on Zulip):

I'd recommend taking a look at Richard Eisenberg's thesis

eddyb (Apr 13 2020 at 23:32, on Zulip):

ahhhhh GHC is attempting to die and go to heaven

centril (Apr 13 2020 at 23:33, on Zulip):

@eddyb what does that mean?

eddyb (Apr 13 2020 at 23:33, on Zulip):

just trying to stretch eternaleye's joke even further :P

centril (Apr 13 2020 at 23:33, on Zulip):

ah

centril (Apr 13 2020 at 23:34, on Zulip):

GHC doubled down on inconsistency there instead of going with cumulative universes or whatnot

varkor (Apr 13 2020 at 23:34, on Zulip):

inconsistency in a UX or semantics sense?

centril (Apr 13 2020 at 23:35, on Zulip):

@varkor "inconsistency as a logic" sense, given Type :: Type

eddyb (Apr 14 2020 at 00:45, on Zulip):

eternaleye made this

eddyb (Apr 14 2020 at 00:47, on Zulip):

@centril ^^

centril (Apr 14 2020 at 00:48, on Zulip):

"What would Girard say" :D

Last update: May 29 2020 at 16:50UTC