Frank 0.1 → 0.2
raw patch · 5 files changed
+433/−15 lines, 5 files
Files
- Frank.cabal +15/−14
- Gubbins.lhs +1/−1
- hello.fk +8/−0
- keylog.fk +119/−0
- test.fk +290/−0
Frank.cabal view
@@ -1,21 +1,22 @@-name: Frank-version: 0.1-synopsis: An experimental programming language with typed algebraic effects-description: An experimental programming language with typed algebraic effects-license: PublicDomain-author: Conor McBride-build-type: Simple-cabal-version: >= 1.8-homepage: http://personal.cis.strath.ac.uk/~conor/pub/Frank/-stability: experimental-category: Languages-license-file: LICENCE-maintainer: conor@strictlypositive.org+name: Frank+version: 0.2+synopsis: An experimental programming language with typed algebraic effects+description: An experimental programming language with typed algebraic effects+license: PublicDomain+author: Conor McBride+build-type: Simple+cabal-version: >= 1.8+homepage: http://personal.cis.strath.ac.uk/~conor/pub/Frank/+stability: experimental+category: Languages+license-file: LICENCE+maintainer: conor@strictlypositive.org+extra-source-files: test.fk hello.fk keylog.fk executable frank main-is: Main.lhs build-depends: base < 5, void, newtype, mtl, she- extensions: TypeOperators, KindSignatures, GADTs, TypeSynonymInstances, FlexibleInstances, GeneralizedNewtypeDeriving, TupleSections, FunctionalDependencies, PatternGuards+ extensions: TypeOperators, KindSignatures, GADTs, TypeSynonymInstances, FlexibleInstances, GeneralizedNewtypeDeriving, TupleSections, FunctionalDependencies, PatternGuards, MultiParamTypeClasses ghc-options: -F -pgmF she other-modules: Gubbins, Pa, Types, Template, Syntax, Check, ElabMonad, Unify, Elab, Run
Gubbins.lhs view
@@ -1,6 +1,6 @@ > {-# OPTIONS_GHC -F -pgmF she #-} > {-# LANGUAGE TypeOperators, FlexibleInstances, FunctionalDependencies,-> RankNTypes #-}+> RankNTypes, MultiParamTypeClasses #-} %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+ hello.fk view
@@ -0,0 +1,8 @@+data List X = nil | X :: (List X)++map {X -> Y} (List X) [] List Y+map f nil = nil+map f (x :: xs) = f x :: map f xs++main [Console] List ()+main = map ouch ('h' :: ('e' :: ('l' :: ('l' :: ('o' :: nil)))))
+ keylog.fk view
@@ -0,0 +1,119 @@+sig ReadLine+ = peek [] Char+ | nom++sig Abort+ = aborting [] {}++abort [Abort] X+abort = aborting ! {}++default {[] X} [Abort ? X] [] X+default d [x] = x+default d [aborting ? k] = d!++{[Abort] X} / {[] X} [] {[] X}+e / d = {default d ? e!}++if Bool then {[] X} else {[] X} [] X+if tt then t else f = t!+if ff then t else f = f!++see Char [ReadLine, Abort] ()+see c = if (peek! =Char= c) then {()} else {abort!}++eat Char [ReadLine, Abort] ()+eat c = see c >> nom!++++() >> Y [] Y+_ >> y = y++X << () [] X+x << _ = x++data List X+ = nil+ | X :: (List X)++data SExp+ = atom (List Char)+ | SExp & SExp++sexp [ReadLine, Abort] SExp+sexp =+ ({see '.' >> abort!} /+ ({eat '(' >> open!} /+ ({see ')' >> abort!} /+ ({eat ' ' >> sexp!} /+ {atom (name!)}+ ))))!++open [ReadLine, Abort] SExp+open =+ ({see '.' >> abort!} /+ ({eat ' ' >> open!} /+ ({eat ')' >> atom nil} /+ {sexp! & cdr!}+ )))!++cdr [ReadLine, Abort] SExp+cdr =+ ({eat ' ' >> cdr!} /+ ({eat '.' >> (sexp! << close!)} /+ {open!}+ ))!++close [ReadLine, Abort] ()+close =+ ({eat ' ' >> close!} /+ ({eat ')'} /+ {abort!}+ ))!++elem Char (List Char) [] Bool+elem c nil = ff+elem c (c' :: cs) = if (c =Char= c') then {tt} else {elem c cs}++name [ReadLine] List Char+name = if (elem (peek!) (' ' :: ('(' :: (')' :: ('.' :: nil)))))+ then {nil}+ else {(peek! << nom!) :: name!}++data Maybe X = no | yes X++let X in {X -> [] Y} [] Y+let x in f = f x++noBS (Maybe Char) [ReadLine ? X] [Console] X+noBS _ [x] = x+noBS no [peek ? k] = let inch! in {c -> noBS (yes c) ? k c}+noBS (yes c) [peek ? k] = noBS (yes c) ? k c+noBS _ [nom ? k] = noBS no ? k ()++data Stk X+ = (Stk X) -peek {Char -> [ReadLine, Abort] X}+ | (Stk X) -nom+ | root {[ReadLine, Abort] X}++withBS (Stk X) (Maybe Char) [ReadLine, Abort ? [{}] X] [Console] X+withBS stk _ [x] = x+withBS stk no [peek ? k] = let inch! in+ { '\b' -> pop stk+ | c -> withBS (stk -peek k) (yes c) ? k c+ }+withBS stk (yes c) [peek ? k] = withBS stk (yes c) ? k c+withBS stk (yes c) [nom ? k] = ouch c >> withBS (stk -nom) no ? k ()+withBS stk _ [aborting ? l] = pop stk++note There's a need for indexing here, to prevent nom! before peek!++pop (Stk X) [Console] X+pop (stk -peek k) = withBS stk no ? k (peek!)+pop (stk -nom) = ouch '\b' >> (ouch ' ' >> (ouch '\b' >> pop stk))+pop (root r) = withBS (root r) no ? r!++main [Console] SExp+main = withBS (root {sexp!}) no ? sexp!+
+ test.fk view
@@ -0,0 +1,290 @@+note+ This is a test source file in the programming language Frank.++note+ Layout in Frank is really dumb. Each left-anchored line begins a new+ top-level block, containing all the tokens until the next left-anchored+ line. Other spacing is unimportant. A block beginning "note" is a comment.++note+ Frank's type system relates three notions+ (1) value types, of things which *are*+ (2) computation types, of things which *do*+ (3) effect signatures, which specify what one *can*++note+ Some perfectly ordinary datatypes follow. List is parametrized.++data Nat+ = zero+ | suc Nat++data List X+ = nil+ | X :: (List X)++note+ Type constructors are always prefix and capitalized.+ Type variables are always capitalized.+ Value constructors are uncapitalized and form *templates*+ with places given by the things which are types.+ So :: is infix.++note+ Here are some perfectly ordinary functions.++Nat + Nat [] Nat+zero + y = y+suc x + y = suc (x + y)++(List X) ++ (List X) [] List X+nil ++ ys = ys+(x :: xs) ++ ys = x :: (xs ++ ys)++note+ These definitions declare a function template, where the types show+ the places for inputs. The [] (pronounced "returns") marks the end+ of the template and the beginning of the output type.+ You can drop [] (), if the output is the unit type.++dull Nat+dull zero = ()+dull (suc n) = dull n++note+ An effect signature is also prefix and capitialized. It describes a+ bunch of commands. Again [] means "returns" and you can drop [] ().++sig State S+ = get [] S+ | set S++note+ Here's how to describe a way to run a stateful process.+ The type [State S ? X] is the type of *requests* from stateful processes.+ A request is either [x] ("return x", where x is an X) or+ [command ? continuation].+ Frank's ? construct allows a function from a request type to+ *handle* a process.++state S [State S ? X] [] X+state s [x] = x+state s [get ? k] = state s ? k s+state _ [set s ? k] = state s ? k ()++note+ Unlike eff, Frank does not automatically compose the handler to the+ continuation. Ultimately, there's no great difference in expressivity,+ but this way is a little more first-order, and it's easier for the+ handler to evolve. Here, for example, we handle the continuation for+ set s using a suitably updated handler.+++note+ Here's the Abort effect signature and one way to run it.+ Frank currently does not allow polymorphic commands, so let's+ use the empty type, {}.++sig Abort+ = aborting [] {}++data Maybe X+ = yes X+ | no++catch [Abort ? X] [] Maybe X+catch [x] = yes x+catch [aborting ? k] = no++note+ To invoke a command with no arguments, use a postfix "!". Without+ arguments, a function symbol stands for the function itself, not the+ result of invoking it. f is pure, but (f !) may not be.++ Our aborting command has no arguments, so needs a !. It returns an+ element of {}, which can be mapped to any type by the postfix {} operator,+ pronounced "bunk".++abort [Abort] X+abort = aborting! {}+++note Nonempty {..}, pronounced "thunk", make a value type from a+ computation type. You can think of a thunk as a "suspended+ computation", and the fact that "suspenders" is American for+ "braces" is handily mnemonic. Frank distinguishes value type X (of+ X values) from value type {[] X} of suspended computations that+ return X values.++ That distinction allows us to write control operators.++note+ Bool is built in, as if+ data Bool = tt | ff++if Bool then {[] X} else {[] X} [] X+if tt then t else e = t!+if ff then t else e = e!++note The above if-then-else chooses which thunk to invoke. To+ construct thunks, write expressions in {..}, so it looks+ suspiciously like C. We may observe that++ catch ? if tt then {zero} else {abort!} = yes zero++ Contrast with the conditional function.++cond Bool X X [] X+cond tt t f = t+cond ff t f = f++note We'll find that++ catch ? cons tt zero (abort!) = no++ because the (abort!) is evaluated.+++note The reason [] is a bracket, not a :, is that it isn't always+ empty. It contains a bunch of signatures for effects the function+ is allowed to do. Here's safe subtraction, which we can write+ directly, thus.++Nat - Nat [Abort] Nat+x - zero = x+zero - suc y = abort!+suc x - suc y = x - y++note+ You can invoke subtraction only where Abort is enabled, e.g., inside+ catch. Frank programs are checked with respect to an ambient bunch of+ signatures. The ? construct locally extends the ambient bunch of+ signatures.++note+ Here's a little higher-order entertainment for you. A function type+ is a computation type, and can thus be thunked. Thunks are always+ pure, even if the function being thunked might perform some effects.+ The inner [] could indeed contain some signatures, and if it does,+ well, those signatures need to be enabled anywhere you *invoke* the+ function.++map {A -> [] B} (List A) [] List B+map f nil = nil+map f (a :: as) = f a :: map f as++note+ You are at liberty to suppress an empty [] in a computation type,+ but be aware! When you write a function type, each [sigs] it contains+ is really an *action* on the ambient signature, meaning "sigs extending+ the ambient signature". That's to say, the types are ever so slightly+ effect-polymorphic. For map, below, the meaning is that whatever effects+ are available when map is invoked may be used at each element, too. Our+ map is really Haskell's "mapM". The upshot is that you can write this:++subs (List Nat) Nat [Abort] List Nat+subs xs n = map {m -> m - n} xs++note+ But there's a subtlety. Consider trees represented with functional+ branching. Each node packs a *pure* function from Bool.++data Tree X+ = leaf X+ | node {Bool -> Tree X}++note+ The following definition of tree mapping is disallowed++ tmap {A -> B} (Tree A) [] Tree B+ tmap f (leaf a) = leaf (f a)+ tmap f (node g) = node {b -> tmap f (g b)}++ The type of f, longhand, is {A -> [] B} meaning that f can do+ whatever the ambient effects are when tmap is invoked. But we+ use f inside a node, where the function must be pure, so the+ typechecker refuses.++ The following is, however, accepted. Here, the signature in f's type+ says {}, which as a signature is pronounced "pure". Its action on+ the ambient signature is to empty it.++tmap {A -> [{}] B} (Tree A) [] Tree B+tmap f (leaf a) = leaf (f a)+tmap f (node g) = node {b -> tmap f (g b)}++note+ You can't make a dangerous, nearly broken tree, like this.++ subt (Tree Nat) Nat [Abort] Tree Nat+ subt xt n = tmap {m -> m - n} xt++note+ But safe mapping is ok.++addt (Tree Nat) Nat [] Tree Nat+addt xt n = tmap {m -> m + n} xt++note+ Of course you can do something like.++mkNode (Tree X) (Tree X) [] Tree X+mkNode l r = node {tt -> l | ff -> r}++tmapOk {A -> B} (Tree A) [] Tree B+tmapOk f (leaf a) = leaf (f a)+tmapOk f (node g) = mkNode (tmapOk f (g tt)) (tmapOk f (g ff))+++note+ Here's a bit of stateful fun.+ The defined command "bong" returns the value of a Boolean state+ but flips it.++not Bool [] Bool+not tt = ff+not ff = tt++X but () [] X+x but c = x++bong [State Bool] Bool+bong = get! but set (not (get!))+++note+ So if we define pairing...++data Pair A B = A & B++note+ ...we get++ state ff ? bong! & bong! = ff & tt+++note+ Bits and Pieces for examples++two [] Nat+two = suc (suc zero)++note+ I must allow the definition of non-functional values.++note+ main [] Nat+ main = two! + two!++note+ main [] Maybe Nat+ main = catch ? if tt then {zero} else {abort!}++note+ main [Abort] List Nat+ main = subs (two ! :: (two ! :: nil)) (suc zero)++main [Console] Char+main = inch!++