Joomy Korkut joom

Reddit discussion.

Disclaimer 1: Type classes are great but they are not the right tool for every job. Enjoy some balance and balance to your balance.

Disclaimer 2: I should tidy this up but probably won’t.

Disclaimer 3: Yeah called it, better to be realistic.

Type classes are a language of their own, this is an attempt to document features and give a name to them.

This document has moved!

It's now here, in The Programmer's Compendium. The content is the same as before, but being part of the compendium means that it's actively maintained.

Principled Meta Programming for Scala

This note outlines a principled way to meta-programming in Scala. It tries to combine the best ideas from LMS and Scala macros in a minimalistic design.

LMS: Types matter. Inputs, outputs and transformations should all be statically typed.
Macros: Quotations are ultimately more easy to deal with than implicit-based type-lifting
LMS: Some of the most interesting and powerful applications of meta-programming

	{-# LANGUAGE CPP #-}
	{-# LANGUAGE ScopedTypeVariables #-}
	{-# LANGUAGE FlexibleInstances, FlexibleContexts #-}
	{-# LANGUAGE DataKinds, GADTs, KindSignatures, TypeOperators, UndecidableInstances #-}

	#if __GLASGOW_HASKELL__ < 708
	#error "requires GHC 7.10 or newer"
	#endif
	module Main (main) where

	(*** Turing Machines in Coq *)

	(** Some preliminary types we'll use *)
	CoInductive CoList (A: Type) := CONS (a:A) (t:CoList A) \| NIL.

	Arguments CONS [A] _ _.
	Arguments NIL [A].

	CoInductive Delay A := HERE (a:A) \| LATER (_:Delay A).

	{-# LANGUAGE DeriveFunctor #-}
	module Bidi where

	-- For 'guard'.
	import Control.Monad
	-- We use Cofree to represent type-annotated terms.
	import Control.Comonad.Cofree
	import Data.Functor.Classes
	-- We use Fix to represent unannotated terms.
	import Data.Functor.Foldable

	{-# LANGUAGE DataKinds #-}
	{-# LANGUAGE FlexibleContexts #-}
	{-# LANGUAGE FlexibleInstances #-}
	{-# LANGUAGE MultiParamTypeClasses #-}
	{-# LANGUAGE PolyKinds #-}
	{-# LANGUAGE TypeFamilies #-}
	{-# LANGUAGE TypeOperators #-}
	{-# LANGUAGE UndecidableInstances #-}

	module Lib where


	open import Algebra
	open import Data.Bool
	open import Data.Empty
	open import Data.List
	open import Data.List.Properties
	open import Data.Nat
	open import Data.Product
	open import Data.Unit
	open import Function


	sequential :: [Int] -> Bool
	sequential = all (==True) (zipWith beside xs (tail xs))
	where
	beside n1 n2 = abs (n2 - n1) == 1

	{-
	λ> sequential [1,2,3]
	True
	λ> sequential [3,2,1]

	module Weed where

	data ⊥ : Set where

	magic : {A : Set} → ⊥ → A
	magic ()

	data Weed (A : Set) : Set where
	grow : (A → Weed A) → Weed A