Flow: Dependent types

[steida]

Like http://www.idris-lang.org. Is this possible?

[gcanti]

@steida worth noting that idris has a JavaScript backend included in the compiler (not sure if is "production ready" though)

[xvw]

Excuse me @steida, i'm little curious. Do you have "pratical uses cases" for using Dependent types for a JavaScript application (except a proof) ? (It is a true question).
Thanks !

[steida]

I have a useful use case. I am in the middle of redesigning Este to typed CSS in JS. "24px" should be valid, "24pfof" not.

[xvw]

I'm not familiar with Flow (my bad) but why not just use a wrapper for px and returns a Phantom type (with generics) ?

[vkurchatkin]

Here is a small example:

class Unit<T:string> {}

type Num<T> = number & Unit<T>;


declare function area(a: Num<'m'>, b: Num<'m'>): Num<'m^2'>;

declare function _(s: number): { meters: Num<'m'>, meter: Num<'m'> };

area(1, 2); // can't do this
area(_(1).meter, _(2).meters); // can do this                            

[gcanti]

Another option without changing the runtime representation

// brands (private)
class IsPixel {}
class IsMedia {}

// CSS types
type Px = string & IsPixel;
type Media = string & IsMedia;

// smart constructors (public)
export function px(value: number): Px {
  return ((`${value}px`: any): Px)
}

export function minHeight(minHeight: Px): Media {
  return ((`@media (minHeight: ${minHeight})`: any): Media)
}

// usage
type DivStyle = {|
  fontSize?: Px,
  lineHeight?: Px | number
  // other rules here...
|};

const style: DivStyle = {
  // fontSize: '30px', // <= error: This type is incompatible with IsPixel
  fontSize: px(30), // <= type safe and the runtime representation is still string
  // a: 1 // <= error: property `a` Property not found in object type 
}

const media: [Media, DivStyle] = [
  minHeight(px(300)), 
  {
    fontSize: px(10)
  }
]

console.log(media) // => ["@media (minHeight: 300px)", ...]

[MichaReiser]

I personally believe that Refinement Types fits better to the model of flow. Dependent Types have the problem to not be inferable. Refinement types are.

There currently exists one implementation for Haskell and TypeScript

[mgtitimoli]

I would find this addition very useful, as it could help on a couple of patterns.

For example, It could provide a way to type some currying cases like the following one:

const setValue = (key: "key1" | "key2") =>
  (destination: Object) =>
    (value: <HERE WE NEED TO RESTRICT VALUE BASED ON KEY>) => ({
      ...destination,
      [key]: value 
    });

[mgtitimoli]

A simple construction similar to ternaries could probably work:

type Value<Key: "key1" | "key2"> = Key is "key1" ? Value1 : Value2;

[mgtitimoli]

Having a deeper look into the subject, I'm not sure if what I'm talking could be thought as dependent types or if they are instead conditional types.

I've just found Typescript provide support on a similar construction of the one I expressed before and it's called conditional types.