vollmerm

{-# LANGUAGE MagicHash #-}
{-# LANGUAGE UnboxedTuples #-}
{-# LANGUAGE CPP #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE Strict #-}
{-# LANGUAGE TypeFamilies #-}

module VectorSum where
import GHC.Exts
import Control.Monad.Primitive

vollmerm

In-place updates and memory layout

Diamond types for in-place updates, extended with lifetimes

As a starting point, example from Hofmann's paper:

append l m =
  case l of
 nil -> m

vollmerm

Deterministic Parallel Programming with Graded Modal Types

I wrote that title because it sounds cool but I don't know if it's actually appropriate. This is a brainstorming document for a few related ideas about parallel programming with linear and modal types.

The structure of this document so far is:

1. some exploration of "pure" parallel programming with mutable data using linear types, and
2. the beginnings of an idea for adapting prior work on DRF programming using "fractional permissions" to graded modal types

There's a bit of a narrative between the two relating to how we can split up "independent" work. First, according to the structure of data (writing to distinct parts of some mutable data), and second according to control flow (classifying data as writable or read-only at different points of a program's execution).

vollmerm

{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE ScopedTypeVariables   #-}

module LatticeSecurity where

data H -- High
data L -- Low

class Flow l l'              where
class Flow l l' => Less l l' where

vollmerm

#lang gibbon

;; use structs/data instead of sexp
(provide typecheck-expr
         Int_ Bool_ Lamt NullT P S N B Begin Lam App Null
	 CONSEXPR NULLEXPR CONSPARAM NULLPARAM CONSTYPE NULLTYPE)

(data ListExpr
      [CONSEXPR Expr ListExpr]
      [NULLEXPR])

vollmerm

#!/usr/bin/env stack
-- stack --resolver lts-13.8 --install-ghc runghc --package criterion
{-# LANGUAGE DeriveGeneric, DeriveAnyClass #-}
import Criterion.Main
import GHC.Generics (Generic)
import Control.DeepSeq

data Tree = Leaf Int | Inner Int Int Tree Tree
          deriving (Eq, Generic, NFData)

vollmerm

 ! Responding to env Var: DEBUG=5
 ! We set DEBUG based on command-line verbose arg: 5
Parsing text: "#lang gibbon\n\n(data Tree\n      (Null)\n      (Leaf Int)\n      (Node Int Tree Tree))\n\n;; (define (buildtree (n : Int)) : Tree\n;;   (helper 0 (- n 1)))\n\n(define (helper (s : Int) (e : Int)) : Tree\n  (if (< e s)\n      (Null)\n      (if (= s e)\n          (Leaf s)\n          (let ((m : Int (+ (div (- e s) 2) s)))\n            (Node m (helper s (- m 1))\n                  (helper (+ m 1) e))))))\n\n(define (copy-tree (tr : Tree)) : Tree\n  (case tr\n    ((Null) (Null))\n    ((Leaf n) (Leaf n))\n    ((Node n1 l r) (Node n1 (copy-tree l) (copy-tree r)))))\n\n(define (sum-tree (tr : Tree)) : Int\n  (case tr\n    ((Null) 0)\n    ((Leaf n) n)\n    ((Node n l r) (+ n (+ (sum-tree l) (sum-tree r))))))\n\n(define (tree-insert (tr : Tree) (n : Int)) : Tree\n  (case tr\n    ((Null)        (Leaf n))\n    ((Leaf n1)     (if (< n n1)\n                       (Node n1 (Leaf n) (Null))\n                       (Node n1 

vollmerm

{-# LANGUAGE DeriveGeneric #-}
{-# LANGUAGE OverloadedStrings #-}
{-# OPTIONS_GHC -Wall #-}

module Lang.Source where

import GHC.Generics

-- This is a quick sketch of a simple source language. Functions can only be defined at the
-- top level, and we need to specify all types at the top level. It's assuming ANF, and all

vollmerm

{-# LANGUAGE DataKinds           #-}
{-# LANGUAGE GADTs               #-}
{-# LANGUAGE KindSignatures      #-}
{-# LANGUAGE TypeOperators       #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# OPTIONS_GHC -fplugin GHC.TypeLits.Normalise #-}

module Data.SizedArray where

import GHC.TypeLits

vollmerm

-- Parallel Bit Climbing
-- climb.hs
-- Mike Vollmer
--
--   This program uses Accelerate to attempt to find the minimum
--   point of the sinbowl function. It uses parallel bit climbing,
--   a form of local search.
--
--   It takes three command-line parameters:
--