The Future of Programming is Dependent Types

Read the example in this excellent blog for explanation of Dependent Type (ie Type depends on its Value) :
eg.

Type ArrayOfOne with value ‘length’ of INT 1.

Type ArrayOfTwo with value ‘length’ of INT 2.

Type ArrayOfThree with value ‘length’ of INT 3.

Then compiler will know if correct (before run time error) :

ArrayOfThree = ArrayOfOne + ArrayOfTwo

or wrong if:

ArrayOfTwo = ArrayOfOne + ArrayOfThree

https://medium.com/background-thread/the-future-of-programming-is-dependent-types-programming-word-of-the-day-fcd5f2634878

Advertisements

Leave a Reply

Fill in your details below or click an icon to log in:

WordPress.com Logo

You are commenting using your WordPress.com account. Log Out /  Change )

Google photo

You are commenting using your Google account. Log Out /  Change )

Twitter picture

You are commenting using your Twitter account. Log Out /  Change )

Facebook photo

You are commenting using your Facebook account. Log Out /  Change )

Connecting to %s