//Normal C# argument X must be nominally int
public void Foo(int x)

//With claims constraints
public void Foo(int x) where x < 10
//You can't call the function without providing claims that 
//meet the constraint

Foo(5)//Literal is compile time known to meet it
Foo(15)//Fails
Foo("5")//Not an int

var bar = 7;

Foo(bar);//Passes because the literal claim carries forward

bar = Random.NextInt();
//Assignment wipes the known claims.

Foo(bar);//Compiler error because it doesn't have the claims

if(foo is < 8) 
{
  Foo(bar);//Allowed now that we have the claim
  //{<8} claim satisifies the {<10} requirement
}

//^This is all what was previous shown, now for some unifying
//This syntax also for you to define claims or sets of them once
//And then reuse them
type IntLessThan10 = int < 10;

object bar = Random.NextInt();
Foo(bar);//Complains because it's both not an int or proven <10

//This is valid C# 11 pattern matching
if(bar is int < 10)
{//It's a type clause with a relation clause
 Foo(bar);//Is proven now
}

//But we should be able to write this purely as a type clause
if(bar is IntLessThan10)//1 clause matches the type
{//The type itself has its own constraints to handle
 Foo(bar);//The type has universal claims of being an int and < 10
 //By universal, I mean 100% of the type an object of that type
 //Always has these properties
}

//That also means we could refactor our method to look like
public void Foo(IntLessThan10 x)

//The entire constraint can be part of the type signature.

//A consequence of this is that when you use where syntax to
//Define a constraint inline, you're just creating an anonymouse type

type A' = int < 10;

//Another implication of this is that the type clause from pattern
//matching should also be liftable into the where clause on the method
//This is already supportable

//We could write the least reusuable, most verbose version of the
//method like this

public void Foo(object x) 
  where x int
  where x < 10
  
//All 3 with the object & 2 anonymouse clauses making anon type
//the type upfront + 1 clause making anon type
//the named type

//They all express the same thing. It's purely named for anonymouse
//typing for the method signature. Both are as strong and static

//This also means that we can produce values with known claims
//This means you don't have to constantly recheck via if statements
//If the value coming out of a method has a guarenteed value.

type PositiveInt32 = int > 0;

public class Array<TValue, PositiveInt32:Size> {}

public PositiveInt32 RandomFromCeiling(PositiveInt32 ceiling)
{
  return Random.Next(1, ceiling);
  //Returns a range claim of 1-ceiling which means the >0
}

var foo = new int[7];//Valid for the Size, since 7 is a PositiveInt32
var foo = new int[0];//Invalid since it's wrong
var bar = RandomFromCeiling(85);

var foo = new int[bar];//Guarenteed to work

//RandomFromCeiling produced a value and we haven't interrogated it
//yet to learn any of its properties, but the type system tells us
//A lot about it. The Bounded Type of PositiveInt32 tell us that
//It's type must be Int32 and that it always passes the > 0 clause

//Normally the type system only tells us the type, Bounded Types
//Explands that to allow us to ensure specific states of types without
//Needing to manually create a duplicate class for each combo

//IE in old C# you'd need to do

public struct PositiveInt32
{

  PositiveInt32(int value)
  {
    if(value is not >0) throw new Exception("Runtime failure");
  }

}

//This has all sorts of negatives
//You cannot inherit from a struct (for good raeson)
//so there is no nominal relationship between PositiveInt32 and int
//This requires jank where you have an IInt interface that both the
//int struct and PositiveInt32 struct implement
//Now somewhere that takes an int in, instead is taking the interface
//Which nows requires 100% of interactions incur boxing and unboxing
//Overhead which involves your pass by value items now generating
//memory pressure via GC

//Also there is no mechanism in C# to ensure you never instantiate
//a PositiveInt32 with an invalid value. So all of your compiler issues
//Will occur at runtime

//^All of the aforementioned downsides are large enough on their
//own to be an immediate no for the C# team.

//Type bounds have none of these types.
type BoundedType = int;//This bounded type is just a type alias
//^ Literally type script's syntax for it

//x doesn't have a nomimal relationship with int, because it is an int
//^ Specifically it's not a subtype, though worth thinking of if it
//shoudld be

//this means you can pass variables of type BoundedType into anywhere
//That takes an int. You can always pass something with claims to
//Something with less restrictive claims that it matches

//Also all reasons that the compiler yells at you for passing the wrong
//parameters in for an argument is around claims missing

//Passing a string parameter to a int argument doesn't fail because
//Of C#'s type checking system. It fails because it lacks the int claim
//a string variable has the string type claim.
//This is in practice identical behavior as the type checking
//But it comes from a more powerful base. The type system operates
//On both type state and type kind information

//Coming back to the Array example
public class Array<TValue, PositiveInt32:Size> {}
//This is making use of both Bound Types for the allowed value
//And Dependent Typing for Size being part of the type

//This ensure at compile time that the array is initialized correclty
//We can also remove runtime bounds checking from indexing now

public TValue this[int index] 
  where index >= 0
  where index < Size
{
  //unsafe code to return data since array is kinda fundamental to
  //memory access
}

//The compiler knows the exact size of each array
//You can never require something outside of the array's bounds
//Thus we don't need to spend the overhead checking the bounds
//This is over 75% the cost of interacting with an array in C#
//An a common thing that devs need unsafe code to turn off for
//Performance gains. Instead we lift the problem to compiler time
//And now get the safety without any performance cost at runtime

//Unanonymous claims aka anonymous bounded types are intended for
//temporary and quick checks. The lifetime of the claim is transient
//The only guarentee is that at the time the claim was asserted it
//was true, were a variable of a bounded type always has those claims

//Expanding from our trivial type alias
type SomeAlias = string;

//To something more useful
type DriverScore = int >= 0 and <= 10;

//We use primitives all of the time to store data because
//A newtype would be overkill. Often times the validity of that data
//Is conveyed via some field name that uses the primitive and
//Various runtime checks

//Bounded types allow us to provide the strong semantics of how
//A type is used while leveraging a primitive for memory storage

//This can also produce interesting interactions when leveraging
//other language features, such as type dependence

type IntRange<int:Floor, int:Ceiling> 
 where Floor < Ceiling
 = int >= Floor and <= Ceiling
 ;

//IntRange has 2 dependent type arguments
//int Floor and int Ceiling
//It has an anonymous bounded type where Floor is less than Ceiling
//This is an int value and there are bounds constrainting the int
//To be within the Floor to Ceiling range

//Now all of proven things are enforced via the type system

var foo = new IntRange<2,9>(5);//5 is correctly between them
var foo = new IntRange<2,9>(-3);//Compiler knows this is an error

//We can also express these with interfaces that back generic math

type Range<TNumber, TNumber:Floor, TNumber:Ceiling> 
  where TNumber : IRelational<TNumber,TNumber,bool> 
  = TNumber >= Floor and <= Ceiling

//This lets us create things like
type ArrayIndex<PositiveInt32:Size> = Range<0,Size> < Size;

var foo = 7;
ArrayIndex<10> bar = foo;//Allowed
//Explaining why

//ArrayIndex is bounded to the type Range<0,Size> and
//Has the extra bound that Range<0,Size> is less than Size

//Digging deeper

//Range<0,Size> is bound to the type int
//It has a floor of 0 and Ceiling of Size
//Size is a dependent type on ArrayIndex
//ArrayIndex<10> means Size of type PositiveInt32 has a value of 10

//The int backing Range<0,Size> is what ultimately backs ArrayIndex
//It's value must be inclusively contained within the floor and ceiliing
//Effect Floor >= Value <= Ceiling (where value is an int)

//Then we add the extra clause that it is less than Size, which adds
//Value < Size, plugging the 7 in for comparison to the bounds system

//You can imagine the check occurring like
int value = 7;

int Size = 10;//Capture the dependent type for Size from ArrayIndex

int Floor = 0;//Literal passed in
int Ceiling = Size;//Passed from ArrayIndex to Range

bool fitsInBounds = Floor <= value && value <= Ceiling//Range check
 && value < Size//Additional bound on ArrayIndex definition
 ;
 
//While the Range<0,10> accepts 10 as a value
//the extra < 10 further slims down the accepted values, so only 0-9
//Are allowed

//This means our array element index access method can become even
//stronger

public TValue this[ArrayIndex<Size> index] => ...;

//All instances of ArrayIndex<Size> are valid indexers
//To Array<T, PositiveInt:Size>

//The first version makes it so any algorithms manually accessing
//an array do it safely

var size = 5;
var elements = new Blurbsk[size];

for(var i = 0; i < Blurbsk.Size; i++)
{

  //We as humans know i should be safe 100% of the time
  var e = elements[i];//Compiler would yell at us
  
  //Currently the claims system cannot enforce this yet
  //We'll assume that for loops produce no claims
  //I know it's trivial for us to inspect and decide this currently
  //But technically all 3 statements in the for loop can be
  //arbitrary code

  if(i is >= 0 and < 5)//Now we've proved that i
  {
    var e = elements[i];//Now it's proven
  }

}

//Using the ArrayIndex type

for(var i = 0; i is ArrayIndex<Size>; i++)
{
  //Now we do have a claims being proven to get here
  var e = elements[i];//We can safely do this
}

//This means we can also have another method return the address to
//something in the array and safely consume it

ArrayIndex<Size> GetRandomIndex<TValue, PositiveInt32:Size>
  (Array<TValue, Size> array)
{

  var rand = Random.NextInt(0, Size - 1);
  //This always should be valid but the claims aren't there
  //Should be someway to improve the language to solve this
  
  return rand is ArrayIndex<Size>//Only uses this if it meets it
    ?? 0//Which does always meet it
    ;

}

//Now we could grab an element safely like

var index = GetRandomIndex(elements);//Type inference fills in args
var el = elements[index];//We can safely know accessing this always
//Will work

//It would also be nice to associative types, so that the ArrayIndex
//Can be pulled from the array instance strongly
//not constructed by the user via ArrayIndex<10>

//Lifting via type dependent should allow a value of the type Type
//To be lifted back up into being a type

public Array<TValue, PositiveInt:Size>
{
  public Type IndexType => ArrayIndex<Size>;
}

//We'd want to be able to do something like

myarray = new Array<string, 50>();

var i = 8;

if(i is myArray.IndexType) {}
//Currently it'll return null
//Since i is an int, and int != Type

//This is made up bad syntax that could fix it

//O wait I solved it

public Array<TValue, PositiveInt:Size>
{
  public type ArrayIndex = ArrayIndex<Size>;
  //This nearly is the C# that does this
  public class ArrayIndex : ArrayIndex<Size> {}
}

//The type keyword declares the Bounded Type definition
//ArrayIndex is namespaced within Array

//Array's namespace is local in the above examples 
//You can imagine via usings statements at the top of some file
Array<5>.ArrayIndex//is a reference to the type ArrayIndex<5>
//The bounded Type is in the simpliest form where it's just an alias

var foo = 3;
Array<5>.ArrayIndex bar = foo;//Should work
ArrayIndex<5> baz = foo;//Is easier than manually namespacing in

//You get a win when you already have an array instance

var myarray = new Array<string, 50>();
myArray.ArrayIndex foo = 15;//We know it works
myArray.ArrayIndex foo = 90;//We know it wont compile

//This scoped (it uses a dependent type from a parent scope)
//bounded type saves us having to pass around 50 everywhere

for(var i = 0; i is ArrayIndex<Size>; i++)
//Becomes
for(var i = 0; i is element.ArrayIndex; i++)