Programming paradigms that change how people think about coding (2014)

Re:Programming paradigms that change how people think about ... by kazinator on Thursday March 07, 2019 @08:42PM (#19334433)

The dependent types example seems underwhelming; rejecting arrays of unlike length at compile time is something I'd expect from a Pascal compiler from 1975.

How about C90: pointer to array of 10 is not compatible with a pointer to array 20:

  int process_array(int (*pa)[20]);

  int main(void)
  {
    int array[10];
    process_array(&array);
    return 0;
  }

GCC:

  array.c: In function ‘main’:
  array.c:6:17: warning: passing argument 1 of ‘process_array’ from incompatible pointer type [-Wincompatible-pointer-types]
    process_array(&array);
                 ^
  array.c:1:5: note: expected ‘int (*)[20]’ but argument is of type ‘int (*)[10]’
   int process_array(int (*pa)[20]);
       ^~~~~~~~~~~~~

[ Parent | on HN ]

Re:Programming paradigms that change how people think about ... by ghayes on Thursday March 07, 2019 @09:26PM (#19334606)

The goal is to get static time checking of dynamic types. For example, if I take two dynamic length arrays and loop n times, appending (optionally?) an element to each array, can you still provide a compile-time check that both arrays are necessarily the same length. It’s much more powerful than what you describe.

[ Parent | on HN ]

Re:Programming paradigms that change how people think about ... by kazinator on Friday March 08, 2019 @11:30AM (#19339048)

  s/you describe/the submitted web page describes/

FTFY

What I describe isn't being posed as "dependent types".

[ Parent | on HN ]

Re:Programming paradigms that change how people think about ... by platz on Thursday March 07, 2019 @09:18PM (#19334583)

here's a full code example in Idris, demonstrating Dependent Types, that's not completely facile:

    import Data.String

    -- takes two integers, and a proof that x < y, and yields an integer
    add : 
      (x : Integer) -> 
      (y : Integer) -> 
      (prf : x < y = True) ->     -- require a proof that that x < y
      Integer
    add x y prf = x + y

    main : IO ()
    main = do
      sx <- getLine -- read string from input
      sy <- getLine -- read string from input
      let Just x = parseInteger sx -- assuming int parse is ok, else error
      let Just y = parseInteger sy -- assuming int parse is ok, else error
      case decEq (x < y) True of   -- decEq constructs a proof (prf) if x < y is True
        Yes prf => print (add x y prf)  -- yes, we got a prf, pass it to add
        No => putStrLn "no prf, x is not less than y"  -- the prf variable is not available in this case

lets say I mess up the sign of the comparison on the case line and write decEq (x > y) instead... then I'd get a type error

    When checking argument prf to function Main.add:
    Type mismatch between
                x > y = True (Type of prf)
        and
                x < y = True (Expected type)

there's no way to construct the prf value artificially, or sneak in different parameters that are unrelated to the prf value.

it's either a compile error or it's valid.

[ Parent | on HN ]

Re:Programming paradigms that change how people think about ... by kyllo on Friday March 08, 2019 @01:35AM (#19335594)

Here's a dependent types example I found a little more interesting: statically modeling a valid date type: https://github.com/chrisdone/sandbox/blob/master/liquid-hask...

[ Parent | on HN ]

Re:Programming paradigms that change how people think about ... by coldtea on Friday March 08, 2019 @06:20AM (#19336622)

>How about C90: pointer to array of 10 is not compatible with a pointer to array 20:

As if that's all dependent types are?

[ Parent | on HN ]

Re:Programming paradigms that change how people think about ... by kazinator on Friday March 08, 2019 @10:38AM (#19338413)

That's what is exemplified by the submitted page as representing the paradigm.

[ Parent | on HN ]