| -- In type theory we can show that ℕ and Bool are not equal as follows | |
| module N≠Bool where | |
| open import Relation.Binary.PropositionalEquality | |
| open import Data.Nat | |
| open import Data.Bool | |
| open import Data.Sum | |
| open import Data.Empty |
| #!/usr/bin/env cabal | |
| {- cabal: | |
| build-depends: base, mtl, containers, uniplate | |
| ghc-options: -Wall | |
| -} | |
| -- | An example of a kind inference for data types using | |
| -- unification-based constraint solving. | |
| -- | |
| -- See the blog post: |
Every once in a while I investigate low-level backend options for PL-s, although so far I haven't actually written any such backend for my projects. Recently I've been looking at precise garbage collection in popular backends, and I've been (like on previous occasions) annoyed by limitations and compromises.
I was compelled to think about a system which accommodates precise relocating GC as much as possible. In one extreme configuration, described in this note, there
| {-# LANGUAGE GADTs #-} | |
| module Main where | |
| import Control.Applicative (liftA2) | |
| data Yaml | |
| = String String | |
| | Object [(String, Yaml)] | |
| deriving Show |
| #!/usr/bin/env cabal | |
| {- cabal: | |
| build-depends: base, mwc-random | |
| ghc-options: -with-rtsopts=-s -Wall | |
| -} | |
| {- | |
| Copyright (C) 1998 Ross Ihaka | |
| Copyright (C) 2000-2014 The R Core Team | |
| Copyright (C) 2007 The R Foundation |
| {-# | |
| LANGUAGE | |
| DeriveGeneric, DeriveDataTypeable, | |
| MultiParamTypeClasses, | |
| ViewPatterns | |
| #-} | |
| -- A short example of an ML-style module system atop a core lambda calculus. | |
| -- | |
| -- The core expression language has variables, applications and | |
| -- lambdas and constants. The type language has variables (of the single kind *) |
