1
Fork 0

Add lunarline

This commit is contained in:
Matei Adriel 2023-10-29 02:10:10 +02:00
parent f055d600fd
commit 1259904c07
10 changed files with 587 additions and 0 deletions

View file

@ -11,6 +11,7 @@
| [existentials](./existentials) | Experiment regarding the Church-encoding of existential types | | [existentials](./existentials) | Experiment regarding the Church-encoding of existential types |
| [gadts](./gadts) | Experiment regarding ways to encode GADTs in Purescript | | [gadts](./gadts) | Experiment regarding ways to encode GADTs in Purescript |
| [lambda-calculus](./lambda-calculus) | Lambda calculus evaluator | | [lambda-calculus](./lambda-calculus) | Lambda calculus evaluator |
| [lunarline](./lunarline) | Attempt at optimizing a functional language using compile-time partial evaluation |
| [lune](./lune) | Failed effect-system project | | [lune](./lune) | Failed effect-system project |
| [maps](./maps) | Attempt at implementing maps with membership proofs | | [maps](./maps) | Attempt at implementing maps with membership proofs |
| [proofs](./proofs) | Attempt at expressing mathematical proofs using Purescript's effect system | | [proofs](./proofs) | Attempt at expressing mathematical proofs using Purescript's effect system |

10
purescript/lunarline/.gitignore vendored Normal file
View file

@ -0,0 +1,10 @@
/bower_components/
/node_modules/
/.pulp-cache/
/output/
/generated-docs/
/.psc-package/
/.psc*
/.purs*
/.psa*
/.spago

72
purescript/lunarline/idea Normal file
View file

@ -0,0 +1,72 @@
map f = case _ of
Nil -> Nil
x:xs -> f x : map f xs
map2 f g xs = map g (map f xs)
----------
map2 f g xs = map g case xs of
Nil -> Nil
x:xs -> f x : map f xs
----------
map2 g f xs = case (case ...) ...
----------
map2 f g xs = case xs of
Nil -> case Nil of
Nil -> Nil
x:xs -> f x : map f xs
x:xs -> case f x : map f xs of
Nil -> Nil
x:xs -> g x : map g xs
----------
map2 f g xs = case xs of
Nil -> Nil
x:xs -> let
a = f x
b = map f xs
in g a : map g b
----------
map2 f g xs = case xs of
Nil -> Nil
x:xs -> g (f x) : map g (map f xs)
----------
map2 f g = case _ of
x:xs -> g (f x) : map2 f g xs
Nil -> Nil
----------
map2 f g = case _ of
x:xs -> (compose g f) x : map2 f g xs
Nil -> Nil
==========
Unify
map2 f g a
with
map u1 u2
u2 = a
==========
Unify
(compose g f) x
with
u1 x
u1 = compose g f
==========
Unify
map2 f g xs
with
map (compose g f) xs
TRUE
map2 = map (compose g f) xs

View file

@ -0,0 +1,104 @@
{-
Welcome to your new Dhall package-set!
Below are instructions for how to edit this file for most use
cases, so that you don't need to know Dhall to use it.
## Use Cases
Most will want to do one or both of these options:
1. Override/Patch a package's dependency
2. Add a package not already in the default package set
This file will continue to work whether you use one or both options.
Instructions for each option are explained below.
### Overriding/Patching a package
Purpose:
- Change a package's dependency to a newer/older release than the
default package set's release
- Use your own modified version of some dependency that may
include new API, changed API, removed API by
using your custom git repo of the library rather than
the package set's repo
Syntax:
where `entityName` is one of the following:
- dependencies
- repo
- version
-------------------------------
let upstream = --
in upstream
with packageName.entityName = "new value"
-------------------------------
Example:
-------------------------------
let upstream = --
in upstream
with halogen.version = "master"
with halogen.repo = "https://example.com/path/to/git/repo.git"
with halogen-vdom.version = "v4.0.0"
with halogen-vdom.dependencies = [ "extra-dependency" ] # halogen-vdom.dependencies
-------------------------------
### Additions
Purpose:
- Add packages that aren't already included in the default package set
Syntax:
where `<version>` is:
- a tag (i.e. "v4.0.0")
- a branch (i.e. "master")
- commit hash (i.e. "701f3e44aafb1a6459281714858fadf2c4c2a977")
-------------------------------
let upstream = --
in upstream
with new-package-name =
{ dependencies =
[ "dependency1"
, "dependency2"
]
, repo =
"https://example.com/path/to/git/repo.git"
, version =
"<version>"
}
-------------------------------
Example:
-------------------------------
let upstream = --
in upstream
with benchotron =
{ dependencies =
[ "arrays"
, "exists"
, "profunctor"
, "strings"
, "quickcheck"
, "lcg"
, "transformers"
, "foldable-traversable"
, "exceptions"
, "node-fs"
, "node-buffer"
, "node-readline"
, "datetime"
, "now"
]
, repo =
"https://github.com/hdgarrood/purescript-benchotron.git"
, version =
"v7.0.0"
}
-------------------------------
-}
let upstream =
https://github.com/purescript/package-sets/releases/download/psc-0.14.3-20210825/packages.dhall sha256:eee0765aa98e0da8fc414768870ad588e7cada060f9f7c23c37385c169f74d9f
in upstream

View file

@ -0,0 +1,35 @@
{-
Welcome to a Spago project!
You can edit this file as you like.
Need help? See the following resources:
- Spago documentation: https://github.com/purescript/spago
- Dhall language tour: https://docs.dhall-lang.org/tutorials/Language-Tour.html
When creating a new Spago project, you can use
`spago init --no-comments` or `spago init -C`
to generate this file without the comments in this block.
-}
{ name = "my-project"
, dependencies =
[ "arrays"
, "console"
, "debug"
, "effect"
, "foldable-traversable"
, "lists"
, "maybe"
, "prelude"
, "profunctor-lenses"
, "psci-support"
, "run"
, "strings"
, "tuples"
, "typelevel"
, "typelevel-prelude"
, "unordered-collections"
, "zipperarray"
]
, packages = ./packages.dhall
, sources = [ "src/**/*.purs", "test/**/*.purs" ]
}

View file

@ -0,0 +1,134 @@
module Lunarline.Ast where
import Prelude
import Data.Array as A
import Data.Array as Array
import Data.Array.NonEmpty (NonEmptyArray)
import Data.Array.NonEmpty as NA
import Data.Foldable (foldl)
import Data.Lens (_2, first, over)
import Data.List as List
import Data.Maybe (Maybe(..))
import Data.String (joinWith)
import Data.Tuple.Nested (type (/\), (/\))
import Lunarline.String (indent, parensWhen)
---------- Types
data Case
= Named String
| Deconstruct String (Array Case)
data Expression
= Var String
| Lambda String Expression
| Call Expression Expression
| Match Expression (NonEmptyArray (Case /\ Expression))
| Let String Expression Expression
| Constructor String
| IgnoreVar String Expression
---------- Helpers
-- | Syntax sugar for creating calls from purescript
callMany :: Expression -> Array Expression -> Expression
callMany f args = A.foldl Call f args
-- | Attempt organizing a constructor call
-- | into the constructor name and the passed arguments
unrollConstructor :: Expression -> Maybe (String /\ Array Expression)
unrollConstructor (Call next argument)
= unrollConstructor next
<#> over _2 (flip Array.snoc argument)
unrollConstructor (Constructor name) = Just (name /\ [])
unrollConstructor _ = Nothing
-- | Checks if a pattern match cases shadows a given variable name
caseShadows :: String -> Case -> Boolean
caseShadows target (Named name) = target == name
caseShadows target (Deconstruct _ children) = A.any (caseShadows target) children
-- | Count the number of times a variable occurs inside an expression.
-- | Takes care of shadowing
occurences :: String -> Expression -> Int
occurences name = go 0
where
go acc (Var var) = if var == name then acc + 1 else acc
go acc (IgnoreVar var expr) = if name == var then acc else go acc expr
go acc (Lambda var expr) = if name == var then acc else go acc expr
go acc (Call function argument) = go (go acc argument) function
go acc (Constructor _) = acc
go acc (Let var value body) = if var == name then inValue else go inValue body
where
inValue = go acc value
go acc (Match expr cases) = foldl processCase (go acc expr) cases
where
processCase acc (thisCase /\ continuation) =
if caseShadows name thisCase then
acc else go acc continuation
-- | Ignore a var which references itself. Useful for avoiding infinite recursion while optimizing
avoidInfiniteRecursion :: String -> Expression -> Expression
avoidInfiniteRecursion var expr
| occurences var expr == 0 = expr
| otherwise = IgnoreVar var expr
---------- Pretty printing
instance Show Case where
show (Named name) = name
show (Deconstruct constructor nested) = constructor <> " "
<> joinWith " " (parensWhen needsParens show <$> nested)
where
needsParens (Named _) = false
needsParens (Deconstruct _ nested) = A.length nested /= 0
instance Show Expression where
show (Var name) = name
show (IgnoreVar var expr) =
if occurences var expr /= 10000 then show expr
else "shadow " <> show var <> ". " <> show expr
show (Constructor name) = name
show lam@(Lambda _ _) = "\\" <> joinWith " " args <> " -> " <> show body
where
args /\ body = collectLambdas lam
show (Let name definition body) = "let " <> name <> " = " <> show definition <> "\nin " <> show body
show (Match expr cases) = "case " <> parensWhen exprNeedsParens show expr <> " of" <> "\n" <> indent 2 prettyCases
where
exprNeedsParens = case _ of
Match _ _ -> true
IgnoreVar _ e -> exprNeedsParens e
_ -> false
prettyCases = joinWith "\n" $ NA.toArray $ printCase <$> cases
printCase (thisCase /\ continuation) = show thisCase <> " ->" <>
if onSeparateLine then "\n" <> indent 2 (show continuation)
else " " <> show continuation
where
onSeparateLine = case continuation of
Match _ _ -> true
IgnoreVar _ _ -> true
Lambda _ _ -> true
Let _ _ _ -> true
_ -> false
show (Call function argument) =
parensWhen leftNeedsParens show function
<> " "
<> parensWhen rightNeedsParens show argument
where
leftNeedsParens = case _ of
Match _ _ -> true
Lambda _ _ -> true
IgnoreVar _ _ -> true
Let _ _ _ -> true
_ -> false
rightNeedsParens = case _ of
Call _ _ -> true
IgnoreVar _ _ -> true
_ -> false
-- | Gruop an expression into it's arguments and it's body.
-- | In case of non lambda expressions the argument array will be empty
collectLambdas :: Expression -> Array String /\ Expression
collectLambdas = go >>> first A.fromFoldable
where
go (Lambda name body) = first (List.Cons name) (go body)
go other = List.Nil /\ other

View file

@ -0,0 +1,163 @@
module Lunarline.Inline where
import Prelude
import Control.Bind (bindFlipped)
import Data.Array as A
import Data.HashMap (HashMap)
import Data.HashMap as HM
import Data.Lens (Lens', over, second)
import Data.Lens.Record (prop)
import Data.Maybe (Maybe(..), fromMaybe)
import Data.Traversable (for)
import Data.Tuple (uncurry)
import Data.Tuple.Nested (type (/\), (/\))
import Data.ZipperArray (ZipperArray)
import Data.ZipperArray as ZA
import Effect.Console (log)
import Effect.Unsafe (unsafePerformEffect)
import Lunarline.Ast (Case(..), Expression(..), avoidInfiniteRecursion, occurences, unrollConstructor)
import Run (Run)
import Run as Run
import Run.Except (FAIL, fail, runFail)
import Run.Reader (READER, asks, local, runReader)
import Type.Proxy (Proxy(..))
import Type.Row (type (+))
---------- Types
type Scope = HashMap String Expression
type Context
=
{ scope :: Scope
}
---------- Monad
-- | The base context most inlining operations run inside
type InlineM r = Run (READER Context r)
-- | Same as InlineM, but might fail
type BreakableInlineM r = InlineM (FAIL + r)
-- | The default context containing no bindings in scope
emptyContext :: Context
emptyContext = { scope: HM.empty }
-- | Run a computation inside the InlineM monad
runInlineM :: forall a. Context -> InlineM () a -> a
runInlineM ctx = runReader ctx >>> Run.extract
---------- Helpers
attempt :: forall r a. (a -> Run (FAIL r) a) -> a -> Run r a
attempt f a = runFail (f a) <#> fromMaybe a
lookupScope :: forall r. String -> InlineM r (Maybe Expression)
lookupScope name = asks (_.scope >>> HM.lookup name)
incorporateFailure :: forall r a. Run (FAIL r) (Maybe a) -> Run (FAIL r) a
incorporateFailure = bindFlipped case _ of
Just success -> pure success
Nothing -> fail
appendScope :: forall r. String -> Expression -> InlineM r ~> InlineM r
appendScope name expression = local
(over _scope $ HM.insert name expression)
dropFromScope :: forall r. String -> InlineM r ~> InlineM r
dropFromScope name = local
(over _scope $ HM.delete name)
extendScopeWith :: forall r. Scope -> InlineM r ~> InlineM r
extendScopeWith extension = local (over _scope $ HM.union extension)
---------- Implementation
executeSafely :: forall r. Expression -> InlineM r ((InlineM r Expression -> InlineM r Expression) /\ Expression)
executeSafely expr = ado
expr <- execute expr
in
go expr
where
go = case _ of
IgnoreVar name body -> (dropFromScope name >>> map (avoidInfiniteRecursion name) >>> restrain) /\ inner
where
restrain /\ inner = go body
other -> identity /\ other
execute :: forall r. Expression -> InlineM r Expression
execute = attempt $ go case _ of
Var name -> do
map (avoidInfiniteRecursion name) $ incorporateFailure $ lookupScope name
IgnoreVar name body -> do
dropFromScope name $ execute body
Call function argument -> do
restrain /\ function <- executeSafely function
restrain' /\ argument <- executeSafely argument
restrain $ restrain' case function of
Lambda name body -> do
appendScope name argument $ execute body
_ -> pure $ Call function argument
Lambda argument body -> do
restrain /\ body <- dropFromScope argument $ executeSafely body
restrain $ pure $ Lambda argument body
Match child cases -> do
restrain /\ child <- executeSafely child
restrain case child of
Match expr innerCases -> execute
$ Match expr
$ second (\c -> Match c cases) <$> innerCases
other -> do
executeMatch other (ZA.fromNonEmptyArray cases)
Let name definition continuation -> do
definition <- execute definition
continuation <- appendScope name definition $ execute continuation
pure
if occurences name definition == 0 && occurences name continuation == 0 then
continuation
else Let name definition continuation
Constructor name -> pure $ Constructor name
where
go f expr = do
res <- f expr
let a = unsafePerformEffect $ log $ "Inlinng: " <> show expr <> "\nwith: " <> show res <> "\n\n\n"
pure res
-- | Attempt to create a scope from a pattern match of some case
-- | over some expression
matchCase
:: Expression -> Case -> Maybe Scope
matchCase expression (Named name) = Just (HM.singleton name expression)
matchCase expression (Deconstruct expectedConstructor childCases)
| Just (name /\ arguments) <- unrollConstructor expression
, name == expectedConstructor
, A.length childCases == A.length arguments =
ado
subMatchResults <- for subMatches (uncurry matchCase)
in A.foldr HM.union HM.empty subMatchResults
where
subMatches = A.zip arguments childCases
matchCase _ _ = Nothing
-- | Execute a pattern match expression
executeMatch
:: forall r
. Expression
-> ZipperArray (Case /\ Expression)
-> BreakableInlineM r Expression
executeMatch child cases = case matchCase child currentCase of
Nothing -> do
case ZA.goNext cases of
Nothing -> ado
cases <- for (ZA.toNonEmptyArray cases) \(currentCase /\ continuation) -> do
-- TODO: when encountering
-- case expr of A a1 ... an -> body
-- replace expr with `A a1 ... an` inside the body
execute continuation <#> (/\) currentCase
in Match child cases
Just remaining -> executeMatch child remaining
Just scopeExtension ->
extendScopeWith scopeExtension $ execute currentContinuation
where
currentCase /\ currentContinuation = ZA.current cases
---------- Lenses
_scope :: Lens' Context Scope
_scope = prop (Proxy :: _ "scope")

View file

@ -0,0 +1,38 @@
module Main where
import Prelude
import Data.Array.NonEmpty as NA
import Data.Tuple.Nested ((/\))
import Effect (Effect)
import Effect.Console (logShow)
import Lunarline.Ast (Case(..), Expression(..), callMany)
import Lunarline.Inline (emptyContext, execute, runInlineM)
myMap :: Expression
myMap = Lambda "h"
$ Lambda "array"
$ Match (Var "array")
$
NA.cons'
( Deconstruct "Cons" [ Named "x", Named "xs" ]
/\ callMany (Constructor "Cons")
[ Call (Var "h") (Var "x")
, callMany (Var "map")
[ Var "h", Var "xs" ]
]
)
[ Deconstruct "Nil" [] /\ Constructor "Nil"
]
myMap2 :: Expression
myMap2 = Let "map" myMap
$ Lambda "f"
$ Lambda "g"
$ Lambda "list"
$ callMany (Var "map") [ Var "g", callMany (Var "map") [ Var "f", Var "list" ] ]
main :: Effect Unit
main = do
logShow myMap2
logShow $ runInlineM emptyContext $ execute myMap2

View file

@ -0,0 +1,19 @@
module Lunarline.String where
import Prelude
import Data.String (Pattern(..), joinWith, split)
-- | Indent a multi line string
indent :: Int -> String -> String
indent amount = split (Pattern "\n") >>> map (indentOne amount) >>> joinWith "\n"
-- | Indents a single line string
indentOne :: Int -> String -> String
indentOne n a
| n <= 0 = a
| otherwise = " " <> indentOne (n - 1) a
-- | Add parenthesis to a pretty printer when a condition holds
parensWhen :: forall a. (a -> Boolean) -> (a -> String) -> a -> String
parensWhen predicate print toPrint = if predicate toPrint then "(" <> print toPrint <> ")" else print toPrint

View file

@ -0,0 +1,11 @@
module Test.Main where
import Prelude
import Effect (Effect)
import Effect.Class.Console (log)
main :: Effect Unit
main = do
log "🍝"
log "You should add some tests."