Web-Projects/blog-static
1
0
Fork 0
Code Issues Pull Requests Releases Wiki Activity

Publish new Idris post.

Browse Source
This commit is contained in:
Danila Fedorin 2020-11-02 01:08:41 -08:00
parent b459e9cbfe
commit 29d12a9914
1 changed files with 5 additions and 8 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

13
content/blog/typesafe_imperative_lang.md
View File

@ -1,8 +1,7 @@
--- ---
title: "A Typesafe Representation of an Imperative Language" title: "A Typesafe Representation of an Imperative Language"
date: 2020-10-30T17:19:59-07:00 date: 2020-11-02T01:07:21-08:00
tags: ["Idris"] tags: ["Idris"]
draft: true
--- ---
A recent homework assignment for my university's programming languages A recent homework assignment for my university's programming languages
@ -85,7 +84,7 @@ can evaluate to either a boolean or an integer value (because a register
can contain either of those types of values). Perhaps we can specify can contain either of those types of values). Perhaps we can specify
the type that an expression evaluates to in the expression's own type: the type that an expression evaluates to in the expression's own type:
`Expr IntTy` would evaluate to integers, and `Expr BoolTy` would evaluate `Expr IntTy` would evaluate to integers, and `Expr BoolTy` would evaluate
to booleans. Then, we could constructors as follows: to booleans. Then, we could have constructors as follows:
```Idris ```Idris
Lit : Int -> Expr IntTy Lit : Int -> Expr IntTy
@ -360,7 +359,7 @@ pattern matching:
The `getReg` function will take out the value of the corresponding The `getReg` function will take out the value of the corresponding
register, returning `Int` or `Bool` depending on the `TypeState`. register, returning `Int` or `Bool` depending on the `TypeState`.
What's important is that if the `TypeState` is known, then so What's important is that if the `TypeState` is known, then so
is the type of `getReg`: no `Either` is involved her, and we is the type of `getReg`: no `Either` is involved here, and we
can directly use the integer or boolean stored in the can directly use the integer or boolean stored in the
register. This is exactly what we do: register. This is exactly what we do:
@ -453,7 +452,7 @@ We then have:
MkState (0, 9, 63) : State (IntTy, IntTy, IntTy) MkState (0, 9, 63) : State (IntTy, IntTy, IntTy)
``` ```
Which seems correct! The program multiplies seven by nine, This seems correct! The program multiplies seven by nine,
and stops when register `A` reaches zero. Our test program and stops when register `A` reaches zero. Our test program
runs, too: runs, too:
@ -473,7 +472,5 @@ aren't possible: our programs are guaranteed to be
{{< sidenote "right" "termination-note" "type correct." >}} {{< sidenote "right" "termination-note" "type correct." >}}
Our programs <em>aren't</em> guaranteed to terminate: Our programs <em>aren't</em> guaranteed to terminate:
we're lucky that Idris' totality checker is turned off by default. we're lucky that Idris' totality checker is turned off by default.
{{< /sidenote >}} {{< /sidenote >}} This was a fun exercise, and I hope you enjoyed reading along!
This was a fun exercise, and I hope you enjoyed reading along!
I hope to see you in my future posts. I hope to see you in my future posts.