| #lang pie | |
| ;; General | |
| (claim Not | |
| (-> U U)) | |
| (define Not | |
| (λ (T) | |
| (-> T Absurd))) |
(Heads up: mostly just playing with ideas and types; no real use cases in sight. Also, I apologize upfront for the silly examples.)
You can use markdown-unlit to load this file as a Literate Haskell file. If you don't want to install it globally on your system, something like this should work:
| {-# LANGUAGE RankNTypes #-} | |
| {-# LANGUAGE ScopedTypeVariables #-} | |
| {-# LANGUAGE TemplateHaskell #-} | |
| module StagedPower where | |
| import Language.Haskell.TH (Q, TExp) | |
| type Code a = Q (TExp a) |
| ---------------------------- MODULE Convergence ---------------------------- | |
| EXTENDS TLC, Integers | |
| abs(n) == IF n < 0 THEN -n ELSE n | |
| (*************************************************************************** | |
| --algorithm Convergence | |
| variables |
| {-# LANGUAGE DeriveFunctor #-} | |
| {-# LANGUAGE DerivingStrategies #-} | |
| {-# LANGUAGE DerivingVia #-} | |
| {-# LANGUAGE KindSignatures #-} | |
| {-# LANGUAGE LambdaCase #-} | |
| {-# LANGUAGE PartialTypeSignatures #-} | |
| {-# LANGUAGE QuantifiedConstraints #-} | |
| {-# LANGUAGE RankNTypes #-} | |
| {-# LANGUAGE ScopedTypeVariables #-} | |
| {-# LANGUAGE BangPatterns #-} |
| {-# LANGUAGE DataKinds #-} | |
| {-# LANGUAGE DerivingStrategies #-} | |
| {-# LANGUAGE FlexibleContexts #-} | |
| {-# LANGUAGE GeneralizedNewtypeDeriving #-} | |
| {-# LANGUAGE PolyKinds #-} | |
| {-# LANGUAGE StandaloneKindSignatures #-} | |
| {-# LANGUAGE TypeFamilies #-} | |
| {-# LANGUAGE RankNTypes #-} | |
| {-# LANGUAGE ScopedTypeVariables #-} | |
| {-# LANGUAGE TypeApplications #-} |
| module StateMachine where | |
| import Data.Foldable (foldlM) | |
| data Init = Init | |
| deriving (Eq, Show) | |
| data A = A Int | |
| deriving (Eq, Show) | |
| data B = B String | |
| deriving (Eq, Show) |
| (ns components-example | |
| (:require [com.stuartsierra.component :as component])) | |
| (defprotocol Counter | |
| (get-c [this]) | |
| (inc-c! [this])) | |
| (defrecord SimpleCounter [counter] | |
| component/Lifecycle | |
| (start [this] |
| {-# LANGUAGE | |
| DataKinds, DeriveGeneric, FlexibleContexts, FlexibleInstances, FunctionalDependencies, | |
| GADTs, MultiParamTypeClasses, ScopedTypeVariables, TypeFamilies, TypeOperators, | |
| UndecidableInstances | |
| #-} | |
| module TypeLevelSets ( | |
| ToSet, Add, Delete, Union, Difference | |
| ) where | |
| import GHC.TypeLits |