<div class="notebook"> <div class="nb-cell markdown" name="md1"> Wende Type inFerence </div> <div class="nb-cell program" data-background="true" data-singleline="true" name="p2"> % Helpers :- op( 500, xfy, [ => ]). :- op( 400, xfy, [ <- ]). :- op( 300, xfy, [ << ]). :- discontiguous(a/4). =>(_, _). <<(Var, (F, Args)) :- app(F, Args, Var, []). <-(L, R) :- let(L, R). </div> <div class="nb-cell program" data-background="true" name="p1"> % Application app(L, R, T2, Meta) :- duplicate_term(L, LCopy), a(LCopy, R, T2, Meta). a(A, [], A, _M). a(A => B, [A | As], T, M) :- a(B, As, T, M). % Unions type((N, Args), N, Args, Inst) :- maplist(inst((N, Args)), Inst). % Create functions to instantiate the type % Currently for sake of copying, even empty inst((Name, Args), ((Name, Args), [])). inst((Name, Args), (X => Result, [X | Xs])) :- inst((Name, Args), (Result, Xs)). % Let let(X, X). </div> <div class="nb-cell program" data-background="true" name="p4"> % Constrained types - Structs, dependent types % F.i {x: 10} = {x: 10, y: 20} % (struct, [field(x, int) | _], ) % fields are unique based on names field(_Field, _Type). % Traits are unique based on name value pairs trait(_Name, _Value). </div> <div class="nb-cell program" data-background="true" name="p3"> % Error cases a(A => _, [Arg | _], _, [(0, wrong_argument, {A, Arg}) | _]). </div> <div class="nb-cell markdown" name="md2"> --- # Basics ### Application For instance a function that takes an `int` and returns an `int` if applied with an `int` will also return an `int` ``` (+) : Int -> Int ``` </div> <div class="nb-cell query" name="q1"> app(int => int, [int], T, []). </div> <div class="nb-cell markdown" name="md3"> ### Multiple arguments An `add` function will always return an int, or a function that adds a constant integer if fed only one argument ``` add : Int -> Int -> Int ``` </div> <div class="nb-cell query" name="q3"> app(int => int => int, [int], T, []). </div> <div class="nb-cell query" name="q5"> app(int => int => int, [int, int], T, []) </div> <div class="nb-cell markdown" name="md5"> ### Polymorphism In fact it works for any type at all </div> <div class="nb-cell query" name="q2"> app(A => A, [A], A, []). </div> <div class="nb-cell markdown" name="md11"> ### Higher order generic functions </div> <div class="nb-cell query" name="q7"> Map = (A => B) => (list, A) => (list, B), Add = int => int => int, app(Add, [int], Add2, []), app(Map, [Add2], AddToAll, []). </div> <div class="nb-cell markdown" name="md4"> You can pass functions around as regular variables ``` fold : (a -> b) -> a -> List a -> List b fold (+) 0 xs ``` </div> <div class="nb-cell query" name="q4"> Fold = (A => B => B) => B => (list, A) => B, Add = int => int => int, app(Fold, [Add, int], Sum, []). </div> <div class="nb-cell markdown" name="md14"> #### Generic functions keep their genericity </div> <div class="nb-cell query" name="q13"> F = A => A => A, app(F, [int, int], int, _) </div> <div class="nb-cell markdown" name="md7"> ### Union Types </div> <div class="nb-cell markdown" name="md8"> {Maybe, Int} </div> <div class="nb-cell query" name="q8"> type(Maybe, maybe, [A], [(Nothing, []), (Just, [A])]), JustOne << (Just, [int]). </div> <div class="nb-cell markdown" name="md9"> #### Destructuring over union types </div> <div class="nb-cell query" name="q9"> % Just A = Just 10 app(Just, [A], JustOne, Err) = app(Just, [int], JustOne, Err). </div> <div class="nb-cell markdown" name="md6"> ## Errors </div> <div class="nb-cell query" name="q12"> app(int => int, [float], _, Err). </div> <div class="nb-cell markdown" name="md12"> ## Big examples </div> <div class="nb-cell query" name="q11"> type(List, list, [A], [ (Nil, []), (Cons, [A, (list, [A])]) ]), Nil2 << (Nil, []), R << (Cons, [int, Nil2]) </div> <div class="nb-cell markdown" name="md13"> #### Sum example ``` sum([]) -> 0 sum(x :: xs) -> x + sum(xs) ``` </div> <div class="nb-cell query" name="q10"> Add = int => int => int, type(List, list, [A], [ (Nil, []), (Cons, [A, (list, [A])]) ]), % sum([])) -> 0 Sum = Nil => int, % --- % e1 = x :: xs E1 << (Cons, [X, Xs]), % sum(e1) -> r2 Sum = E1 => R2, % rest = sum(xs) Rest << (Sum, [Xs]), % r = x + sum R2 << (Add, [X, SumRest]). </div> <div class="nb-cell markdown" name="md10"> ### Thoughts for future - Constrained types (f.i Int without 0, positive int) - Types that inherit ( Number > Int > PositiveInt ) - Side-effects as a separate type system (or a constraint of functions?) ``` openFile : String =[FS.READ]> String stdio : String =[IO.WRITE]> () ``` </div> </div>