Compare commits
4 Commits
5108acba61
...
0ec38537f4
| Author | SHA1 | Date |
|---|---|---|
 rhiannon morris
|
0ec38537f4 | |
|
rhiannon morris
|
1e7423fffe | |
|
rhiannon morris
|
8d401ab404 | |
|
rhiannon morris
|
be46a2fc5c |
7
Makefile
7
Makefile
|
|
@ -29,9 +29,10 @@ LAANTAS_SCRIPT = $(TMPDIR)/laantas-script
|
|||
ALL_TAGS = $(TMPDIR)/all-tags
|
||||
POST_LISTS = $(TMPDIR)/post-lists
|
||||
NICE_DATE = $(TMPDIR)/nice-date
|
||||
SLUG_TAGS = $(TMPDIR)/slug-tags
|
||||
EXECS = \
|
||||
$(LANGFILTER) $(LAANTAS_SCRIPT) \
|
||||
$(ALL_TAGS) $(POST_LISTS) $(NICE_DATE)
|
||||
$(ALL_TAGS) $(POST_LISTS) $(NICE_DATE) $(SLUG_TAGS)
|
||||
|
||||
CABAL_FLAGS ?= -O -v0
|
||||
|
||||
|
|
@ -67,7 +68,8 @@ define pandoc
|
|||
pandoc -s --toc --template $(TEMPLATEDIR)/$(1).html -o $@ $< \
|
||||
-f markdown+emoji \
|
||||
$(SYNTAXFLAGS) \
|
||||
--filter $(LANGFILTER) --filter $(NICE_DATE) --mathjax
|
||||
--filter $(LANGFILTER) --filter $(NICE_DATE) --filter $(SLUG_TAGS) \
|
||||
--mathjax
|
||||
endef
|
||||
|
||||
|
||||
|
|
@ -89,6 +91,7 @@ $(LAANTAS_SCRIPT): lang/laantas-script/* ; $(call cabal-exe)
|
|||
$(ALL_TAGS): $(BLOG_META_DEPS) ; $(call cabal-exe,blog-meta:)
|
||||
$(POST_LISTS): $(BLOG_META_DEPS) ; $(call cabal-exe,blog-meta:)
|
||||
$(NICE_DATE): $(BLOG_META_DEPS) ; $(call cabal-exe,blog-meta:)
|
||||
$(SLUG_TAGS): $(BLOG_META_DEPS) ; $(call cabal-exe,blog-meta:)
|
||||
|
||||
define cabal-exe
|
||||
@echo "[build] $(notdir $@)"
|
||||
|
|
|
|||
|
|
@ -15,7 +15,6 @@ import qualified YAML
|
|||
import System.Environment
|
||||
import qualified Data.Text.IO as Text
|
||||
import qualified Data.Text as Text
|
||||
import Data.Char
|
||||
|
||||
|
||||
main :: IO ()
|
||||
|
|
@ -36,8 +35,8 @@ getTags file = do
|
|||
makeYAML :: [Set Text] -> LazyBS.ByteString
|
||||
makeYAML tags = "---\n" <> yaml <> "\n...\n" where
|
||||
yaml = YAML.encode1 $ YAML.obj
|
||||
[("title" ##= YAML.str "all tags"),
|
||||
("tags" ##= collate tags)]
|
||||
[("title" ##= YAML.str "all tags"),
|
||||
("all-tags" ##= collate tags)]
|
||||
|
||||
makeMake :: [Set Text] -> Text
|
||||
makeMake tags' = Text.unlines $ build : allPosts : map makeRule tags where
|
||||
|
|
@ -46,7 +45,7 @@ makeMake tags' = Text.unlines $ build : allPosts : map makeRule tags where
|
|||
t <- ["all-tags", "index"] <> map slug' tags]
|
||||
makeRule' opt title file =
|
||||
"$(TMPDIR)/" <> file <> ".md : $(POSTS) $(POST_LISTS)\n\
|
||||
\\t@echo \"[post-lists] $<\"\n\
|
||||
\\t@echo \"[post-lists] " <> file <> "\"\n\
|
||||
\\t$(POST_LISTS) " <> opt <> " --out $@ \\\n\
|
||||
\\t $(POSTSDIR) \"" <> title <> "\""
|
||||
allPosts = makeRule' "" "all posts" "index"
|
||||
|
|
@ -70,25 +69,19 @@ instance YAML.ToYAML Tag where
|
|||
[("name" ##= name), ("slug" ##= slug), ("count" ##= count)]
|
||||
|
||||
collate :: [Set Text] -> [Tag]
|
||||
collate tags₀ =
|
||||
toList $ fst $ foldl' add1 (mempty, mempty) $ foldMap toList tags₀
|
||||
collate =
|
||||
toList . foldl' add1 mempty . foldMap toList
|
||||
where
|
||||
add1 (tags, slugs) name
|
||||
| Map.member name tags =
|
||||
(Map.adjust incrCount name tags, slugs)
|
||||
| otherwise =
|
||||
let tag = makeTag slugs name in
|
||||
(Map.insert name tag tags,
|
||||
Set.insert (slug tag) slugs)
|
||||
makeTag slugs name =
|
||||
Tag {name, slug = makeSlug slugs name, count = 1}
|
||||
makeSlug slugs name = head $ filter (`notElem` slugs) candidates where
|
||||
slug₀ = Text.map toSlugChar name
|
||||
toSlugChar c
|
||||
| isAlphaNum c && isAscii c || c == '-' = toLower c
|
||||
| otherwise = '_'
|
||||
candidates = slug₀ : [slug₀ <> Text.pack (show i) | i <- [(0 :: Int) ..]]
|
||||
incrCount t@(Tag {count}) = t {count = succ count}
|
||||
add1 tags name = Map.alter (add1' tag) (slug tag) tags
|
||||
where tag = makeTag name
|
||||
|
||||
add1' new Nothing = Just new
|
||||
add1' new (Just old)
|
||||
| name new == name old = Just (old {count = succ (count old)})
|
||||
| otherwise = error $ "slug collision between " <> show (name old) <>
|
||||
" and " <> show (name new)
|
||||
|
||||
makeTag name = Tag {name, slug = makeSlug name, count = 1}
|
||||
|
||||
data Options =
|
||||
Opts {
|
||||
|
|
|
|||
|
|
@ -50,3 +50,8 @@ executable nice-date
|
|||
import: deps, exe
|
||||
hs-source-dirs: .
|
||||
main-is: nice-date.hs
|
||||
|
||||
executable slug-tags
|
||||
import: deps, exe
|
||||
hs-source-dirs: .
|
||||
main-is: slug-tags.hs
|
||||
|
|
|
|||
|
|
@ -3,6 +3,10 @@ module Misc where
|
|||
import qualified System.Console.GetOpt as GetOpt
|
||||
import System.Environment
|
||||
import System.Exit
|
||||
import Data.Text (Text)
|
||||
import qualified Data.Text as Text
|
||||
import Data.Char (isAlphaNum, isAscii, toLower)
|
||||
import Text.Pandoc.Definition
|
||||
|
||||
-- | exception on 'Left'
|
||||
unwrap :: Show a => FilePath -> Either a b -> IO b
|
||||
|
|
@ -20,3 +24,34 @@ getOptionsWith hdr mkDef descrs = do
|
|||
putStrLn $ GetOpt.usageInfo (hdr prog) descrs
|
||||
exitFailure
|
||||
|
||||
makeSlug :: Text -> Text
|
||||
makeSlug name = Text.map toSlugChar name where
|
||||
toSlugChar c
|
||||
| isAlphaNum c && isAscii c || c == '-' = toLower c
|
||||
| otherwise = '_'
|
||||
|
||||
|
||||
toTextList :: MetaValue -> Maybe [Text]
|
||||
toTextList (MetaList vs) = traverse toText vs
|
||||
toTextList _ = Nothing
|
||||
|
||||
toText :: MetaValue -> Maybe Text
|
||||
toText (MetaString str) = Just str
|
||||
toText (MetaInlines is) = foldMap inlineText is
|
||||
toText (MetaBlocks bs) = foldMap blockText bs
|
||||
toText _ = Nothing
|
||||
|
||||
inlineText :: Inline -> Maybe Text
|
||||
inlineText (Str txt) = Just txt
|
||||
inlineText Space = Just " "
|
||||
inlineText SoftBreak = Just " "
|
||||
inlineText LineBreak = Just " "
|
||||
inlineText (RawInline _ txt) = Just txt
|
||||
inlineText _ = Nothing
|
||||
|
||||
blockText :: Block -> Maybe Text
|
||||
blockText (Plain is) = foldMap inlineText is
|
||||
blockText (Para is) = foldMap inlineText is
|
||||
blockText Null = Just ""
|
||||
blockText (RawBlock _ txt) = Just txt
|
||||
blockText _ = Nothing
|
||||
|
|
|
|||
|
|
@ -1,19 +1,16 @@
|
|||
import Text.Pandoc.Definition
|
||||
import Data.Map.Strict (Map)
|
||||
import qualified Data.Map.Strict as Map
|
||||
import Data.Time
|
||||
import Text.Pandoc.JSON
|
||||
import Data.Text (Text, unpack, pack)
|
||||
import Data.Text (unpack, pack)
|
||||
import Data.Char (toLower)
|
||||
import Misc
|
||||
|
||||
main :: IO ()
|
||||
main = toJSONFilter \(Pandoc (Meta m) body) -> do
|
||||
m' <- niceDate m
|
||||
m' <- Map.alterF reformat "date" m
|
||||
pure $ Pandoc (Meta m') body
|
||||
|
||||
niceDate :: Map Text MetaValue -> IO (Map Text MetaValue)
|
||||
niceDate = Map.alterF reformat "date"
|
||||
|
||||
reformat :: Maybe MetaValue -> IO (Maybe MetaValue)
|
||||
reformat Nothing = pure Nothing
|
||||
reformat (Just (toText -> Just txt)) = do
|
||||
|
|
@ -22,24 +19,3 @@ reformat (Just (toText -> Just txt)) = do
|
|||
let str = formatTime defaultTimeLocale "%A %-e %B %Y" (date :: Day)
|
||||
pure $ Just $ MetaString $ pack $ map toLower str
|
||||
reformat (Just d) = fail $ "date is\n" <> show d <> "\nwanted a string"
|
||||
|
||||
toText :: MetaValue -> Maybe Text
|
||||
toText (MetaString str) = Just str
|
||||
toText (MetaInlines is) = foldMap inlineText is
|
||||
toText (MetaBlocks bs) = foldMap blockText bs
|
||||
toText _ = Nothing
|
||||
|
||||
inlineText :: Inline -> Maybe Text
|
||||
inlineText (Str txt) = Just txt
|
||||
inlineText Space = Just " "
|
||||
inlineText SoftBreak = Just " "
|
||||
inlineText LineBreak = Just " "
|
||||
inlineText (RawInline _ txt) = Just txt
|
||||
inlineText _ = Nothing
|
||||
|
||||
blockText :: Block -> Maybe Text
|
||||
blockText (Plain is) = foldMap inlineText is
|
||||
blockText (Para is) = foldMap inlineText is
|
||||
blockText Null = Just ""
|
||||
blockText (RawBlock _ txt) = Just txt
|
||||
blockText _ = Nothing
|
||||
|
|
|
|||
|
|
@ -0,0 +1,21 @@
|
|||
import Text.Pandoc.Definition
|
||||
import qualified Data.Map.Strict as Map
|
||||
import Text.Pandoc.JSON
|
||||
import Data.Text (Text)
|
||||
import Misc
|
||||
|
||||
main :: IO ()
|
||||
main = toJSONFilter \(Pandoc (Meta m) body) -> do
|
||||
m' <- Map.alterF addSlugs "tags" m
|
||||
pure $ Pandoc (Meta m') body
|
||||
|
||||
addSlugs :: Maybe MetaValue -> IO (Maybe MetaValue)
|
||||
addSlugs Nothing = pure Nothing
|
||||
addSlugs (Just (toTextList -> Just tags)) =
|
||||
pure $ Just $ MetaList $ map addSlug1 tags
|
||||
addSlugs (Just t) = fail $
|
||||
"'tags' is\n" <> show t <> "\nwanted a list of strings"
|
||||
|
||||
addSlug1 :: Text -> MetaValue
|
||||
addSlug1 tag = MetaMap $ Map.fromList
|
||||
[("name", MetaString tag), ("slug", MetaString $ makeSlug tag)]
|
||||
|
|
@ -1,7 +1,7 @@
|
|||
---
|
||||
title: digitle in maude
|
||||
date: 2022-03-14
|
||||
tags: [maude, computer]
|
||||
tags: [maude, computer, cool languages]
|
||||
...
|
||||
|
||||
so you know [digitle] right. it's the countdown numbers round.
|
||||
|
|
|
|||
|
|
@ -0,0 +1,76 @@
|
|||
---
|
||||
date: 2022-07-12
|
||||
title: a few undocumented beluga features
|
||||
tags: [computer, beluga, cool languages]
|
||||
toc: true
|
||||
...
|
||||
|
||||
|
||||
several of these are in the [examples], just not in the documentation. but some
|
||||
of them i did find while looking through the parser.
|
||||
|
||||
[examples]: https://github.com/Beluga-lang/Beluga/tree/master/examples
|
||||
|
||||
|
||||
## unicode
|
||||
|
||||
you can call your context variables `Γ` and it works just fine.
|
||||
you can also use `→` and `⇒` and `⊢` if they are legible in the font you're
|
||||
using.
|
||||
|
||||
|
||||
## block values in substitutions
|
||||
|
||||
a lot of the time you have a variable typed like
|
||||
`\[Γ, b : block (x : term, t : oft x A[..]) ⊢ ty]`,
|
||||
but you actually need a
|
||||
`\[Γ, x : term, t : oft x A[..] ⊢ ty]`,
|
||||
with the block flattened out. or vice versa.
|
||||
or you want to substitute the block more conveniently.
|
||||
|
||||
for this purpose, there is actually a block literal syntax `<a; b; c>` usable
|
||||
in substitutions:
|
||||
|
||||
```beluga
|
||||
let [Γ, b : block (x : term, t : oft x A[..]) ⊢ X] = blah in
|
||||
[Γ, x : term, t : oft x A[..] ⊢ X[.., <x; t>]]
|
||||
|
||||
% but equivalent to this, but clearer (imo)
|
||||
let [Γ, block (x : term, t : oft x A[..]) ⊢ X[.., b.x, b.t]] = blah in
|
||||
[Γ, x : term, t : oft x A[..] ⊢ X]
|
||||
```
|
||||
|
||||
## explicit binders before patterns
|
||||
|
||||
sometimes in a case expression, the type of the pattern variables is too hard
|
||||
for beluga to work out on its own. in this case you get an error message about
|
||||
a stuck unification problem.
|
||||
|
||||
most of the time you can get out of this by writing the types of some variables
|
||||
explicitly. the syntax is like a forall-type:
|
||||
|
||||
```beluga
|
||||
case [Γ ⊢ #p] of
|
||||
| {#p : [Γ ⊢ term]}
|
||||
[Γ, y : term ⊢ #p[..]] ⇒ ?body
|
||||
```
|
||||
|
||||
|
||||
## mutual recursion
|
||||
|
||||
of course this exists. but it's not mentioned anywhere in the documentation for
|
||||
some reason. the syntax is this:
|
||||
|
||||
```beluga
|
||||
LF term : type = …
|
||||
and elim : type = …;
|
||||
|
||||
rec eval-term : (Γ : ctx) [Γ ⊢ term] → [Γ ⊢ value] = …
|
||||
and rec eval-elim : (Γ : ctx) [Γ ⊢ elim] → [Γ ⊢ value] = …;
|
||||
|
||||
inductive ReduceTerm : (Γ : ctx) [Γ ⊢ term] → ctype = …
|
||||
and inductive ReduceElim : (Γ : ctx) [Γ ⊢ elim] → ctype = …;
|
||||
```
|
||||
|
||||
two `rec`s! which is because you can mix `rec`/`proof`, or
|
||||
`inductive`/`coinductive`/`stratified`, within a block.
|
||||
|
|
@ -0,0 +1,436 @@
|
|||
---
|
||||
title: a little ats program
|
||||
date: 2022-09-16
|
||||
tags: [computer, ATS, cool languages]
|
||||
show-toc: true
|
||||
...
|
||||
|
||||
[ats] is a language that is a little infamous among type system likers, for its
|
||||
complexity, its weird syntax, and its thin documentation. well i won't be beat,
|
||||
so here's a little implementation of simply-typed lambda calculus. right now it
|
||||
doesn't actually use many ats-specific features, since i just didn't end up
|
||||
needing them.
|
||||
|
||||
[ats]: http://www.ats-lang.org
|
||||
|
||||
it does leak memory without gc though, so maybe i should have.
|
||||
oh well one thing at a time
|
||||
|
||||
# installation, et cetera
|
||||
|
||||
instead of trying to install ats myself, i just used [nix], since i already
|
||||
have it installed as the least annoying package manager for idris. i just run
|
||||
`nix shell nixpkgs#ats2` and i'm in a shell with `patscc` and `patsopt`
|
||||
available. if you want to try building it yourself, that's, uh, your choice.
|
||||
|
||||
[nix]: https://nixos.org
|
||||
|
||||
to compile the program, i wrote a makefile. just a small one!
|
||||
|
||||
```makefile
|
||||
ATSCC := patscc
|
||||
ATSFLAGS := \
|
||||
-DATS_MEMALLOC_GCBDW -lgc \
|
||||
-atsccomp \
|
||||
'gcc -I$${PATSHOME} -I$${PATSHOME}/ccomp/runtime \
|
||||
-L$${PATSHOME}/ccomp/atslib/lib -std=gnu99'
|
||||
|
||||
%: %.dats
|
||||
$(ATSCC) $< $(ATSFLAGS) -o $@
|
||||
```
|
||||
|
||||
(in some installs the compiler is just called `atscc` for some reason.)
|
||||
|
||||
the first line of `ATSFLAGS` tells it which allocator to use. in this case,
|
||||
`libgc`. the rest tells it to use `-std=gnu99`, so that it can find `alloca()`;
|
||||
the rest is the same as the default.
|
||||
|
||||
one last thing. the first two lines of the program have to be this. i didn't
|
||||
look into it too hard but they seem to define... something... and if you forget
|
||||
to include them the c output by ats isn't even syntactically correct. ouch.
|
||||
|
||||
```ats
|
||||
#include "share/atspre_define.hats"
|
||||
#include "share/atspre_staload.hats"
|
||||
```
|
||||
|
||||
# types
|
||||
|
||||
let's start by defining the syntax for types. it's going to be a single base
|
||||
type, and functions.
|
||||
|
||||
$$
|
||||
\newcommand\Typ{\mathit{typ}}
|
||||
\newcommand\OR{\mathrel|}
|
||||
\Typ ::= \bullet \OR \Typ_1 \to \Typ_2
|
||||
$$
|
||||
|
||||
so obviously, my first attempt was to just write this:
|
||||
|
||||
```ats
|
||||
datatype typ = Base | Arr of (typ, typ)
|
||||
```
|
||||
|
||||
i'm going to need to check two types for equality, so let's do that next.
|
||||
|
||||
```ats
|
||||
fun eq_typ (a : typ, b : typ) .<a>. :<> bool =
|
||||
case (a, b) of
|
||||
| (Base(), Base()) => true
|
||||
| (Arr(a1, a2), Arr(b1, b2)) => eq_typ(a1, b1) && eq_typ(a2, b2)
|
||||
| (_, _) => false
|
||||
```
|
||||
|
||||
alas: (it is talking about the `.<a>.`)
|
||||
|
||||
```
|
||||
/home/niss/ats/lam.dats: 149(line=7, offs=33) -- 150(line=7, offs=34):
|
||||
error(2): the static identifier [a] is unrecognized.
|
||||
```
|
||||
|
||||
surprise! as far as i can tell ats only allows termination checking to be
|
||||
based on _static_ (compile time) information. so i need to index the
|
||||
datatype with, uh, something. when we define functions on syntax like this,
|
||||
they basically always recurse on a subterm. so the height of the syntax tree
|
||||
will do. what i _actually_ have are these more messy definitions.
|
||||
|
||||
```ats
|
||||
datatype typ(int) =
|
||||
| Base(1)
|
||||
| {h1, h2 : nat} Arr(1 + max(h1, h2)) of (typ(h1), typ(h2))
|
||||
|
||||
typedef typ = [h : nat] typ(h)
|
||||
```
|
||||
|
||||
the base type $\bullet$ has height 1, and an arrow type has a height one more
|
||||
than the max height of its subterms. `nat` is a version of `int` constrained to
|
||||
be at least zero, rather than a separate type, so that's why it says `int` one
|
||||
place and `nat` the other. the typechecker has a linear arithmetic solver for
|
||||
reasoning about inequalities and expressions like `1 + max(h1, h2)`.
|
||||
|
||||
i don't want to be talking about "types of height $h$" unless i really have to,
|
||||
though, so there's a definition for just _a_ type too. the syntax `[x : t1] t2`
|
||||
is an existential type that is automatically wrapped and unwrapped, so in this
|
||||
case it is a `typ(h)` for some, unknown, `h`. also, names can be overloaded by
|
||||
their arity so `typ(h)` and `typ` can both be defined in the same scope.
|
||||
|
||||
so now `eq_typ` has to have a more intricate type to talk about height. the
|
||||
definition is still the same though.
|
||||
|
||||
```ats
|
||||
fun eq_typ {ha : nat} .<ha>. (a : typ(ha), b : typ) :<> bool =
|
||||
case (a, b) of
|
||||
| (Base(), Base()) => true
|
||||
| (Arr(a1, a2), Arr(b1, b2)) => eq_typ(a1, b1) && eq_typ(a2, b2)
|
||||
| (_, _) => false
|
||||
|
||||
overload = with eq_typ
|
||||
```
|
||||
|
||||
since i only actually need to care about one of the arguments' height for the
|
||||
termination proof, the other can still just be a `typ`. the last line lets me
|
||||
write `a = b` instead of `eq_typ(a, b)`, which is nice.
|
||||
|
||||
next, i want to be able to print types. ideally this would be a function that
|
||||
returns a string, but string stuff involves pointer weirdness i haven't worked
|
||||
out yet. so it just prints. the only two precedence levels in these types are
|
||||
"left of an arrow" and "not left of an arrow", so that can just be a `bool`.
|
||||
unfortunately `print` has no information about its termination behaviour so
|
||||
there's no point bothering with that stuff here either. :confused:
|
||||
|
||||
```ats
|
||||
fun print_typ (parens : bool, t : typ) : void =
|
||||
case t of
|
||||
| Base() => print "•"
|
||||
| Arr(a, b) => begin
|
||||
if parens then print("(");
|
||||
print_typ(true, a);
|
||||
print(" → ");
|
||||
print_typ(false, b);
|
||||
if parens then print(")");
|
||||
end
|
||||
|
||||
fn print_typ (t : typ) : void = print_typ(false, t)
|
||||
overload print with print_typ
|
||||
```
|
||||
|
||||
# terms
|
||||
|
||||
types are done, now let's move on to terms. we just want names, lambdas, and
|
||||
application.
|
||||
|
||||
$$
|
||||
\newcommand\Term{\mathit{term}}
|
||||
\newcommand\Var{\mathit{var}}
|
||||
\Term ::= \Var \OR \lambda \Var : \Typ. \Term \OR \Term_1 \; \Term_2
|
||||
$$
|
||||
|
||||
for the same reason as before, terms are indexed by their height, but _also_ by
|
||||
the number of variables in scope, since i want de bruijn indices to be
|
||||
intrinsically well-scoped. why even have a type system otherwise. so a
|
||||
`term(n, h)` has $n$ variables and height $h$.
|
||||
|
||||
```ats
|
||||
datatype term(int, int) =
|
||||
| {n, i : nat | i < n} Var(n, 1) of int(i)
|
||||
| {n, h : nat} Lam(n, 1 + h) of (typ, term(1 + n, h))
|
||||
| {n, h1, h2 : nat} App(n, 1 + max(h1, h2)) of (term(n, h1), term(n, h2))
|
||||
|
||||
typedef term(n : int) = [h : nat] term(n, h)
|
||||
```
|
||||
|
||||
a variable is [a de bruijn index][db], which is a natural less than `n`. to
|
||||
express this we need to bridge the static world, where `n` lives, and the
|
||||
dynamic, where `Var`'s field lives. to do this i use a singleton type
|
||||
`int(i)`, whose only value is `i` itself. with this type, you can constraint the
|
||||
static `i`, and in turn the value of the field.
|
||||
|
||||
[db]: https://en.wikipedia.org/wiki/De_Bruijn_index
|
||||
|
||||
|
||||
# contexts
|
||||
|
||||
```ats
|
||||
typedef ctx(n: int) = list(typ, n)
|
||||
```
|
||||
|
||||
a typing context is just a list of types of the appropriate length. since
|
||||
there's no binding in types here, that's all we need.
|
||||
|
||||
looking up into a context is just list lookup, with some constraints to make it
|
||||
work.
|
||||
|
||||
```ats
|
||||
fun lookup {n, i : nat | i < n} .<n>. (g : ctx(n), i : nat(i)) :<> typ =
|
||||
let val+ list_cons(x, g) = g in
|
||||
if i = 0 then x else lookup(g, i - 1)
|
||||
end
|
||||
```
|
||||
|
||||
from the constraints $n \ge 0, i \ge 0, i < n$, the compiler can see that, as
|
||||
$n \ge 1$, the list is nonempty and `list_cons` _is_ the only case. it can also
|
||||
propagate the $i \ne 0$ condition from the `else` to see the recursive call is
|
||||
ok too, and this function is total.
|
||||
|
||||
:::aside
|
||||
while writing this post i discovered that this is actually a restatement of
|
||||
the type of `xs[i]` in the standard library and i could have just used that.
|
||||
oops!
|
||||
:::
|
||||
|
||||
|
||||
# typechecker
|
||||
|
||||
i'm going to write the type checker using exceptions for error handling, because
|
||||
using an error monad without `do` notation was just too annoying. but from the
|
||||
outside it is still going to use a `result` type.
|
||||
|
||||
```ats
|
||||
datatype result(t@ype, t@ype) =
|
||||
| {a, e : t@ype} Ok(a, e) of a
|
||||
| {a, e : t@ype} Err(a, e) of e
|
||||
```
|
||||
|
||||
the funky looking `t@ype` refers to a type of unknown size, as opposed to `type`
|
||||
which can only be instantiated with pointer-sized types. that will not come up
|
||||
again here but "`t@ype`" is definitely the funniest part of ats's syntax.
|
||||
|
||||
the errors we need here are:
|
||||
|
||||
- a function takes an argument of type $A$, but is given one of type $B$;
|
||||
- a term of a non-arrow type is being applied.
|
||||
|
||||
```ats
|
||||
datatype err =
|
||||
| Clash of (typ, typ)
|
||||
| NotArr of typ
|
||||
|
||||
fn print_err (e : err) : void = … // incredibly uninteresting
|
||||
overload print with print_err
|
||||
|
||||
|
||||
typedef typ_res = result(typ, err)
|
||||
|
||||
fn print_res (r : typ_res) : void = …
|
||||
overload print with print_res
|
||||
```
|
||||
|
||||
so onto the typechecker. like i said, it's going to use a local exception for
|
||||
errors, but then catch it on the outside so that it has a pure type.
|
||||
|
||||
```ats
|
||||
fn typ_of {n : nat} (g : ctx n, t : term(n)) :<> typ_res =
|
||||
let
|
||||
exception ERR of err
|
||||
fun go {n, h : nat} .<h>. (g : ctx(n), t : term(n, h)) :<!exn> typ =
|
||||
case t of
|
||||
| Var(i) => lookup(g, i)
|
||||
| Lam(a, t) => Arr(a, go(list_cons(a, g), t))
|
||||
| App(s, t) => begin
|
||||
case go(g, s) of
|
||||
| Arr(a1, b) =>
|
||||
let val a2 = go(g, t) in
|
||||
if a1 = a2 then b else $raise ERR(Clash(a1, a2))
|
||||
end
|
||||
| b => $raise ERR(NotArr(b))
|
||||
end
|
||||
in
|
||||
$effmask_exn(try Ok(go(g, t)) with ~ERR(e) => Err(e))
|
||||
end
|
||||
|
||||
fn typ_of (t : term(0)) :<> typ_res = typ_of(list_nil, t)
|
||||
```
|
||||
|
||||
most of this is fine. a bit noisy i guess. but there are a couple of new things:
|
||||
|
||||
- in the type of `go`, the `:<!exn>` part means it can throw exceptions, but has
|
||||
no other effects.
|
||||
- `$effmask_exn(e)` hides the `exn` effect in `e`, because ats doesn't
|
||||
distinguish different exceptions in effects so it can't tell that `ERR` is the
|
||||
only one that is ever raised.
|
||||
- exceptions are linear, and the pattern `~ERR(e)` is consuming the outermost
|
||||
constructor.
|
||||
- exceptions are the only reason we needed `alloca` in this program
|
||||
:woozy_face:
|
||||
|
||||
|
||||
# the end
|
||||
|
||||
ok, a quick `main` function, and that's it!
|
||||
|
||||
```ats
|
||||
implement main0() = begin
|
||||
print("type of [λx:•. x] is: ");
|
||||
print(typ_of(Lam(Base, Var(0))));
|
||||
print("\ntype of [λx:•. x x] is: ");
|
||||
print(typ_of(Lam(Base, App(Var(0), Var(0)))));
|
||||
print("\n")
|
||||
end
|
||||
```
|
||||
|
||||
and it works, at least on these two examples.
|
||||
|
||||
```
|
||||
type of [λx:•. x] is: • → •
|
||||
type of [λx:•. x x] is: expected an arrow type, but got [•]
|
||||
```
|
||||
|
||||
uh. thank's for reading. maybe i'll write another one if i think of another
|
||||
nice little program that actually uses more of ats's weirdness.
|
||||
|
||||
--------------------------------------------------------------------------------
|
||||
|
||||
<details>
|
||||
<summary>full code</summary>
|
||||
```ats
|
||||
#include "share/atspre_define.hats"
|
||||
#include "share/atspre_staload.hats"
|
||||
|
||||
datatype typ(int) =
|
||||
| Base(1)
|
||||
| {h1, h2 : nat} Arr(1 + max(h1, h2)) of (typ(h1), typ(h2))
|
||||
|
||||
typedef typ = [h : nat] typ(h)
|
||||
|
||||
fun eq_typ {ha : nat} .<ha>. (a : typ(ha), b : typ) :<> bool =
|
||||
case (a, b) of
|
||||
| (Base(), Base()) => true
|
||||
| (Arr(a1, a2), Arr(b1, b2)) => eq_typ(a1, b1) && eq_typ(a2, b2)
|
||||
| (_, _) => false
|
||||
overload = with eq_typ
|
||||
|
||||
fun print_typ (parens : bool, t : typ) : void =
|
||||
case t of
|
||||
| Base() => print "•"
|
||||
| Arr(a, b) => begin
|
||||
if parens then print("(");
|
||||
print_typ(true, a);
|
||||
print(" → ");
|
||||
print_typ(false, b);
|
||||
if parens then print(")");
|
||||
end
|
||||
|
||||
fn print_typ (t : typ) : void = print_typ(false, t)
|
||||
overload print with print_typ
|
||||
|
||||
|
||||
datatype term(int, int) =
|
||||
| {n, i : nat | i < n} Var(n, 1) of int(i)
|
||||
| {n, h : nat} Lam(n, 1 + h) of (typ, term(1 + n, h))
|
||||
| {n, h1, h2 : nat} App(n, 1 + max(h1, h2)) of (term(n, h1), term(n, h2))
|
||||
|
||||
typedef term(n : int) = [h : nat] term(n, h)
|
||||
|
||||
|
||||
typedef ctx(n: int) = list(typ, n)
|
||||
|
||||
fun lookup {n, i : nat | i < n} .<n>. (g : ctx(n), i : int(i)) :<> typ =
|
||||
let val+ list_cons(x, g) = g in
|
||||
if i = 0 then x else lookup(g, i - 1)
|
||||
end
|
||||
|
||||
|
||||
datatype result(t@ype, t@ype) =
|
||||
| {a, e : t@ype} Ok(a, e) of a
|
||||
| {a, e : t@ype} Err(a, e) of e
|
||||
|
||||
|
||||
datatype err =
|
||||
| Clash of (typ, typ)
|
||||
| NotArr of typ
|
||||
|
||||
fn print_err (e : err) : void =
|
||||
case e of
|
||||
| Clash(a, b) => begin
|
||||
print("clash between types [");
|
||||
print(a);
|
||||
print("] and [");
|
||||
print(b);
|
||||
print("]");
|
||||
end
|
||||
| NotArr(t) => begin
|
||||
print("expected an arrow type, but got [");
|
||||
print(t);
|
||||
print("]");
|
||||
end
|
||||
overload print with print_err
|
||||
|
||||
|
||||
typedef typ_res = result(typ, err)
|
||||
|
||||
fn print_res (r : typ_res) : void =
|
||||
case r of Ok(t) => print(t) | Err(e) => print(e)
|
||||
overload print with print_res
|
||||
|
||||
|
||||
fn typ_of {n : nat} (g : ctx n, t : term(n)) :<> typ_res =
|
||||
let
|
||||
exception ERR of err
|
||||
fun go {n, h : nat} .<h>. (g : ctx(n), t : term(n, h)) :<!exn> typ =
|
||||
case t of
|
||||
| Var(i) => lookup(g, i)
|
||||
| Lam(a, t) => Arr(a, go(list_cons(a, g), t))
|
||||
| App(s, t) => begin
|
||||
case go(g, s) of
|
||||
| Arr(a1, b) =>
|
||||
let val a2 = go(g, t) in
|
||||
if a1 = a2 then b else $raise ERR(Clash(a1, a2))
|
||||
end
|
||||
| b => $raise ERR(NotArr(b))
|
||||
end
|
||||
in
|
||||
$effmask_exn(try Ok(go(g, t)) with ~ERR(e) => Err(e))
|
||||
end
|
||||
|
||||
fn typ_of (t : term(0)) :<> typ_res = typ_of(list_nil, t)
|
||||
|
||||
|
||||
implement main0() = begin
|
||||
print("type of [λx:•. x] is: ");
|
||||
print(typ_of(Lam(Base, Var(0))));
|
||||
print("\ntype of [λx:•. x x] is: ");
|
||||
print(typ_of(Lam(Base, App(Var(0), Var(0)))));
|
||||
print("\n")
|
||||
end
|
||||
```
|
||||
</details>
|
||||
|
|
@ -394,14 +394,15 @@ aside {
|
|||
|
||||
|
||||
.kw { color: hsl(300deg, 60%, 30%); }
|
||||
.pp { color: hsl(343deg, 100%, 40%); font-weight: 500; }
|
||||
.dt { color: hsl(173deg, 100%, 24%); font-weight: 500; }
|
||||
.fu { color: hsl(34deg, 100%, 30%); font-weight: 500; }
|
||||
.va { color: hsl(203deg, 100%, 30%); font-weight: 500; }
|
||||
.cf { color: hsl(276deg, 75%, 35%); font-weight: 500; }
|
||||
.pp { color: hsl(343deg, 100%, 40%); /* font-weight: 500; */ }
|
||||
.dt { color: hsl(173deg, 100%, 24%); /* font-weight: 500; */ }
|
||||
.fu { color: hsl(34deg, 100%, 30%); /* font-weight: 500; */ }
|
||||
.va { color: hsl(203deg, 100%, 30%); /* font-weight: 500; */ }
|
||||
.cf { color: hsl(276deg, 75%, 35%); /* font-weight: 500; */ }
|
||||
.op { color: hsl(220deg, 40%, 33%); }
|
||||
.co { color: hsl(221deg, 10%, 39%); font-style: italic; }
|
||||
.bu { color: hsl(100deg, 85%, 30%); font-weight: 500; }
|
||||
.bu { color: hsl(120deg, 85%, 25%); }
|
||||
:is(.st, .fl, .dv, .sc) { color: hsl(143deg, 100%, 20%); }
|
||||
.wa { color: hsl(350deg, 80%, 25%); text-decoration: wavy 1.5px underline; }
|
||||
.al { color: hsl(350deg, 80%, 25%); }
|
||||
.cn { color: hsl(343deg, 100%, 30%); }
|
||||
|
|
|
|||
|
|
@ -0,0 +1,210 @@
|
|||
<?xml version="1.0" encoding="UTF-8"?>
|
||||
<!DOCTYPE language SYSTEM "language.dtd" [
|
||||
<!ENTITY LETTER "A-Za-z\xc0-\xd6\xd8-\xf6\xf8-\xff">
|
||||
<!ENTITY IDENT "[&LETTER;_@$][&LETTER;0-9_@$']*">
|
||||
<!ENTITY ESC "(\\[ntbr'"\\]|\\[0-9]{3}|\\x[0-9A-Fa-f]{2})">
|
||||
<!ENTITY DEC "([0-9][0-9_]*)">
|
||||
<!ENTITY DECEXP "([eE][+-]?&DEC;)">
|
||||
<!ENTITY HEX "([0-9a-fA-F]+)">
|
||||
]>
|
||||
|
||||
<language name="ATS" section="Sources" extensions="*.sats;*.dats;*.hats"
|
||||
version="1" kateversion="5.53">
|
||||
<highlighting>
|
||||
<list name="decl">
|
||||
<item>abstype</item> <item>abst@ype</item> <item>absprop</item>
|
||||
<item>absview</item> <item>absvtype</item> <item>absvt@ype</item>
|
||||
<item>absviewtype</item> <item>absviewt@ype</item>
|
||||
|
||||
<item>exception</item>
|
||||
|
||||
<item>datatype</item> <item>dataprop</item> <item>dataview</item>
|
||||
<item>dataviewtype</item> <item>datavtype</item> <item>datasort</item>
|
||||
|
||||
<item>typedef</item> <item>propdef</item> <item>viewdef</item>
|
||||
<item>vtypedef</item> <item>viewtypedef</item> <item>sortdef</item>
|
||||
<item>tkindef</item> <item>classdec</item>
|
||||
<item>macdef</item> <item>macrodef</item>
|
||||
|
||||
<item>withtype</item> <item>withprop</item> <item>withview</item>
|
||||
<item>withvtype</item> <item>withviewtype</item>
|
||||
|
||||
<item>val</item> <item>fun</item> <item>fn</item> <item>fnx</item>
|
||||
<item>prfun</item> <item>prfn</item> <item>praxi</item>
|
||||
<item>castfn</item>
|
||||
<item>and</item>
|
||||
|
||||
<item>var</item> <item>prvar</item>
|
||||
|
||||
<item>infix</item> <item>infixl</item> <item>infixr</item>
|
||||
<item>prefix</item> <item>postfix</item> <item>nonfix</item>
|
||||
|
||||
<item>symintr</item> <item>symelim</item>
|
||||
|
||||
<item>sta</item> <item>stacst</item>
|
||||
<item>stadef</item> <item>static</item>
|
||||
</list>
|
||||
|
||||
<list name="meta">
|
||||
<item>extern</item> <item>extype</item> <item>extvar</item>
|
||||
<item>$extern</item> <item>$extype</item> <item>$extkind</item>
|
||||
<item>$extype_struct</item>
|
||||
|
||||
<item>$myfilename</item> <item>$mylocation</item> <item>$myfunction</item>
|
||||
|
||||
<item>import</item> <item>staload</item> <item>dynload</item>
|
||||
</list>
|
||||
|
||||
<list name="preproc">
|
||||
<item>#include</item> <item>#staload</item> <item>#dynload</item>
|
||||
<item>#require</item>
|
||||
|
||||
<item>#if</item> <item>#ifdef</item> <item>#ifndef</item>
|
||||
<item>#then</item>
|
||||
<item>#elif</item> <item>#elifdef</item> <item>#elifndef</item>
|
||||
<item>#else</item> <item>#endif</item>
|
||||
|
||||
<item>#error</item> <item>#prerr</item> <item>#print</item>
|
||||
<item>#assert</item>
|
||||
|
||||
<item>#define</item> <item>#undef</item>
|
||||
|
||||
<item>#pragma</item> <item>#codegen2</item> <item>#codegen3</item>
|
||||
</list>
|
||||
|
||||
<list name="impl">
|
||||
<item>assume</item> <item>reassume</item>
|
||||
<item>implmnt</item> <item>implement</item>
|
||||
<item>primplmnt</item> <item>primplement</item>
|
||||
<item>overload</item>
|
||||
</list>
|
||||
|
||||
<list name="expr">
|
||||
<item>begin</item> <item>end</item>
|
||||
<item>op</item> <item>as</item>
|
||||
|
||||
<item>case</item> <item>prcase</item> <item>of</item> <item>when</item>
|
||||
<item>scase</item>
|
||||
|
||||
<item>let</item> <item>local</item> <item>in</item> <item>rec</item>
|
||||
<item>if</item> <item>then</item> <item>else</item>
|
||||
<item>ifcase</item> <item>sif</item>
|
||||
<item>where</item>
|
||||
|
||||
<item>for</item> <item>do</item>
|
||||
<item>$break</item> <item>$continue</item>
|
||||
|
||||
<item>lam</item> <item>llam</item> <item>lam@</item>
|
||||
<item>fix</item> <item>fix@</item>
|
||||
|
||||
<item>try</item> <item>with</item> <item>$raise</item>
|
||||
|
||||
<item>$delay</item> <item>$ldelay</item>
|
||||
|
||||
<item>$arrpsz</item> <item>$arrptrsize</item>
|
||||
<item>$tyrep</item> <item>$d2ctype</item>
|
||||
|
||||
<item>$effmask</item>
|
||||
<item>$effmask_ntm</item> <item>$effmask_exn</item>
|
||||
<item>$effmask_ref</item> <item>$effmask_wrt</item>
|
||||
<item>$effmask_all</item>
|
||||
|
||||
<item>$lst</item> <item>$lst_t</item> <item>$lst_vt</item>
|
||||
<item>$list</item> <item>$list_t</item> <item>$list_vt</item>
|
||||
|
||||
<item>$rec</item> <item>$rec_t</item> <item>$rec_vt</item>
|
||||
<item>$record</item> <item>$record_t</item> <item>$record_vt</item>
|
||||
|
||||
<item>$tup</item> <item>$tup_t</item> <item>$tup_vt</item>
|
||||
<item>$tuple</item> <item>$tuple_t</item> <item>$tuple_vt</item>
|
||||
|
||||
<item>$solver_assert</item>
|
||||
<item>$solver_verify</item>
|
||||
|
||||
<item>$vararg</item>
|
||||
<item>$showtype</item>
|
||||
<item>$tempenver</item>
|
||||
</list>
|
||||
|
||||
<list name="prim">
|
||||
<item>type</item> <item>t@ype</item>
|
||||
<item>view</item> <item>prop</item>
|
||||
<item>viewtype</item> <item>viewt@ype</item>
|
||||
<item>vtype</item> <item>vt@ype</item>
|
||||
</list>
|
||||
|
||||
<list name="const">
|
||||
<item>bool</item> <item>true</item> <item>false</item>
|
||||
<item>int</item> <item>nat</item>
|
||||
</list>
|
||||
|
||||
<contexts>
|
||||
<context attribute="default" lineEndContext="#stay" name="default">
|
||||
<Detect2Chars attribute="comment" context="comment-1"
|
||||
char="/" char1="/" />
|
||||
<Detect2Chars attribute="comment" context="comment-c"
|
||||
char="/" char1="*" />
|
||||
<Detect2Chars attribute="comment" context="comment-ml"
|
||||
char="(" char1="*" />
|
||||
|
||||
<keyword attribute="decl" context="#stay" String="decl" />
|
||||
<keyword attribute="meta" context="#stay" String="meta" />
|
||||
<keyword attribute="preproc" context="#stay" String="preproc" />
|
||||
<keyword attribute="impl" context="#stay" String="impl" />
|
||||
<keyword attribute="expr" context="#stay" String="expr" />
|
||||
<keyword attribute="prim" context="#stay" String="prim" />
|
||||
<keyword attribute="const" context="#stay" String="const" />
|
||||
|
||||
<RegExpr attribute="arrowlike" context="#stay"
|
||||
String="[-=<>:]|=/?=>>?|\.<|>\." />
|
||||
|
||||
<DetectChar attribute="string" context="string" char=""" />
|
||||
|
||||
<RegExpr attribute="decint" context="#stay" String="~?&DEC;" />
|
||||
<RegExpr attribute="float" context="#stay"
|
||||
String="~?((&DEC;\.&DEC;?|\.&DEC;)&DECEXP;?|&DEC;&DECEXP;)" />
|
||||
<RegExpr attribute="hexint" context="#stay" String="~?0[xX]&HEX;" />
|
||||
</context>
|
||||
|
||||
<context attribute="comment" lineEndContext="#pop" name="comment-1" />
|
||||
<context attribute="comment" lineEndContext="#stay" name="comment-c">
|
||||
<!-- not nestable -->
|
||||
<Detect2Chars attribute="comment" context="#pop"
|
||||
char="*" char1="/" />
|
||||
</context>
|
||||
<context attribute="comment" lineEndContext="#stay" name="comment-ml">
|
||||
<!-- nestable -->
|
||||
<Detect2Chars attribute="comment" context="comment-ml"
|
||||
char="(" char1="*" />
|
||||
<Detect2Chars attribute="comment" context="#pop"
|
||||
char="*" char1=")" />
|
||||
</context>
|
||||
|
||||
<context attribute="string" lineEndContext="#stay" name="string">
|
||||
<RegExpr attribute="esc" context="#stay" String="&ESC;" />
|
||||
<DetectChar attribute="string" context="#pop" char=""" />
|
||||
</context>
|
||||
</contexts>
|
||||
|
||||
<itemDatas>
|
||||
<itemData name="default" defStyleNum="dsNormal" />
|
||||
<itemData name="comment" defStyleNum="dsComment" />
|
||||
|
||||
<itemData name="decl" defStyleNum="dsDataType" />
|
||||
<itemData name="meta" defStyleNum="dsKeyword" />
|
||||
<itemData name="preproc" defStyleNum="dsPreprocessor" />
|
||||
<itemData name="impl" defStyleNum="dsFunction" />
|
||||
<itemData name="expr" defStyleNum="dsControlFlow" />
|
||||
<itemData name="prim" defStyleNum="dsBuiltIn" />
|
||||
<itemData name="const" defStyleNum="dsConstant" />
|
||||
|
||||
<itemData name="arrowlike" defStyleNum="dsOperator" />
|
||||
|
||||
<itemData name="string" defStyleNum="dsString" />
|
||||
<itemData name="decint" defStyleNum="dsDecVal" />
|
||||
<itemData name="float" defStyleNum="dsFloat" />
|
||||
<itemData name="hexint" defStyleNum="dsBaseN" />
|
||||
<itemData name="esc" defStyleNum="dsSpecialChar" />
|
||||
</itemDatas>
|
||||
</highlighting>
|
||||
</language>
|
||||
|
|
@ -8,7 +8,7 @@ $endif$
|
|||
|
||||
$if(posts)$
|
||||
$postlist()$
|
||||
$elseif(tags)$
|
||||
$elseif(all-tags)$
|
||||
$taglist()$
|
||||
$endif$
|
||||
|
||||
|
|
|
|||
|
|
@ -13,7 +13,7 @@ $head()$
|
|||
tags:
|
||||
<ul>
|
||||
$for(tags)$
|
||||
<li><a href=/tag-$it$.html>$it$</a>
|
||||
<li><a href=/tag-$it.slug$.html>$it.name$</a>
|
||||
$endfor$
|
||||
</ul>
|
||||
</nav>
|
||||
|
|
|
|||
|
|
@ -1,6 +1,6 @@
|
|||
<main>
|
||||
<ul class=tag-list>
|
||||
$for(tags)$
|
||||
$for(all-tags)$
|
||||
<li>
|
||||
<a href=tag-$it.slug$.html>$it.name$</a>
|
||||
<span class=count>($it.count$)</span>
|
||||
|
|
|
|||
Loading…
Reference in New Issue