search

BartoszMilewski / DaoFP

The Dao of Functional Programming
291 stars 17 forks source link

If Haskell has dependent types, why not laws? #22

Open rks987 opened 3 months ago

rks987 commented 3 months ago

This is a great description of functional programming and the associated Category theory.

I was surprised to learn that Haskell has dependent types, though I gather they aren't completely implemented. Still , if you have dependent types then there is no reason you can't have types representing propositions, and hence laws. So I think you should be a bit more nuanced when you say "you can't express the laws in Haskell". Perhaps just add "yet".

For example here is the Semigroup Behaviour in the toy programming language I'm working on::

`Semigroup = # ` introduces a new identifier
    behaviour of Type by 
        {'Type=>Type: `T = $; # T is the conforming type
            ['  `op: T*T=>T; # NB. T*T=Tuple(T,T)
                `associative: 
                    ∀%{' T*T*T => Type: (`u,`v,`w) = $; # unpack input
                         Eq%(T)(op(op(u,v),w),op(u,op(v,w)))
                      };
            ] # this type is a Structure
        }; # a conforming type must provide values of types op and associative