edsko

#!/bin/bash

if [ ! -n "$1" ]; then
	export ACTIVATED=""

	if [ -n "$PRE_ACTIVATED_PATH" ]; then
		export PATH="$PRE_ACTIVATED_PATH"
		unset PRE_ACTIVATED_PATH
	fi

edsko

{-# LANGUAGE DataKinds             #-}
{-# LANGUAGE FlexibleInstances     #-}
{-# LANGUAGE GADTs                 #-}
{-# LANGUAGE KindSignatures        #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE PolyKinds             #-}
{-# LANGUAGE ScopedTypeVariables   #-}
{-# LANGUAGE TypeApplications      #-}
{-# LANGUAGE TypeFamilies          #-}
{-# LANGUAGE UndecidableInstances  #-}

edsko

newtype Nat (n :: N) = UnsafeInt Int
  deriving Show via Int

data IsNat (n :: N) where
  IsZero ::          IsNat Z
  IsSucc :: Nat n -> IsNat (S n)

toIsNat :: Nat n -> IsNat n
toIsNat (UnsafeInt 0) = unsafeCoerce IsZero
toIsNat (UnsafeInt n) = unsafeCoerce (IsSucc (UnsafeInt (pred n)))

edsko

{-# LANGUAGE DataKinds     #-}
{-# LANGUAGE GADTs         #-}
{-# LANGUAGE PolyKinds     #-}
{-# LANGUAGE RankNTypes    #-}
{-# LANGUAGE TypeFamilies  #-}
{-# LANGUAGE TypeOperators #-}

{-# OPTIONS_GHC -Wall #-}

module TypeLevelComposition where

edsko

-- | Pattern match on 'HasField'
--
-- This is intended to be used together with 'matchHasField'. Example usage:
--
-- > data Foo a
-- >
-- > instance HasField "fooX" (Foo a) Int where ..
-- > instance HasField "fooY" (Foo a) [a] where ..
-- >
-- > _example :: Foo Char -> (Int, [Char])

edsko

{-# LANGUAGE ConstraintKinds       #-}
{-# LANGUAGE DataKinds             #-}
{-# LANGUAGE DeriveGeneric         #-}
{-# LANGUAGE FlexibleContexts      #-}
{-# LANGUAGE FlexibleInstances     #-}
{-# LANGUAGE GADTs                 #-}
{-# LANGUAGE InstanceSigs          #-}
{-# LANGUAGE KindSignatures        #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE PolyKinds             #-}

edsko

{-# LANGUAGE PatternSynonyms #-}
{-# LANGUAGE RoleAnnotations #-}
{-# LANGUAGE TypeFamilies    #-}
{-# LANGUAGE ViewPatterns    #-}

{-# OPTIONS_GHC -Wall #-}

module RoleTest where

import GHC.Exts

edsko

{-# LANGUAGE DeriveDataTypeable   #-}
{-# LANGUAGE FlexibleContexts     #-}
{-# LANGUAGE StandaloneDeriving   #-}
{-# LANGUAGE UndecidableInstances #-}

module Main where

import Data.Char
import Data.Generics
import Data.Reflection

edsko

{-# LANGUAGE FlexibleInstances   #-}
{-# LANGUAGE GADTs               #-}
{-# LANGUAGE RankNTypes          #-}
{-# LANGUAGE ScopedTypeVariables #-}

module NicerData where

import Data.Functor.Const
import Data.Functor.Identity
import Data.Typeable

edsko

module PHOAS where

import Data.Bifunctor
import Data.Functor.Const
import Data.Kind
import Data.SOP.NP
import GHC.Show
import Unsafe.Coerce (unsafeCoerce)

{-------------------------------------------------------------------------------