Skip to content

Instantly share code, notes, and snippets.

@i-am-tom

i-am-tom/First_Main.hs

Last active Apr 25, 2020
Embed
What would you like to do?
Code from streams!
{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE DeriveGeneric #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}
module Main where
import Data.Void (Void)
import Data.Kind (Type)
import GHC.Generics
data User
= User
{ name :: String
, age :: Int
, likesDogs :: Bool
}
deriving (Eq, Generic, Ord, Show)
type HKDify (x :: Type) (f :: Type -> Type)
= GHKDify (Rep x) f
type family GHKDify (rep :: Type -> Type) (f :: Type -> Type) :: Type -> Type where
GHKDify (M1 index metadata inner) f
= M1 index metadata (GHKDify inner f)
GHKDify V1 f
= V1
GHKDify (left :+: right) f
= GHKDify left f :+: GHKDify right f
GHKDify U1 f
= U1
GHKDify (left :*: right) f
= GHKDify left f :*: GHKDify right f
GHKDify (K1 R x) f
= K1 R (f x)
-- Higher-kinded data (HKD)
data UserF (f :: Type -> Type)
= UserF
{ nameF :: f String
, ageF :: f Int
, likesDogsF :: f Bool
}
deriving (Generic)
-- e.g. HKD User f
newtype HKD (x :: Type) (f :: Type -> Type)
= HKD { runHKD :: HKDify x f Void }
-- Don't worry too much about this - we'll explain this in more detail next time {{{
class GDestruct (rep :: Type -> Type) (f :: Type -> Type) where
gdestruct
:: rep Void
-> GHKDify rep f Void
instance GDestruct inner f
=> GDestruct (M1 index metadata inner) f where
gdestruct (M1 inner) = M1 (gdestruct @_ @f inner)
instance (GDestruct left f, GDestruct right f)
=> GDestruct (left :*: right) f where
gdestruct (left :*: right)
= gdestruct @_ @f left :*: gdestruct @_ @f right
instance Applicative f => GDestruct (K1 R x) f where
gdestruct (K1 x) = K1 (pure x)
class Destruct (x :: Type) (f :: Type -> Type) where
destruct :: x -> HKD x f
instance (Generic x, GDestruct (Rep x) f)
=> Destruct x f where
destruct = HKD . gdestruct @_ @f . from
eg0 :: HKD User Maybe
eg0 = destruct (User "Tom" 26 True)
-- }}}
-- construct :: Applicative f => UserF f -> f User
-- construct UserF{..}
-- = User <$> nameF <*> ageF <*> likesDogsF
--
-- destruct User{..}
-- = UserF
-- { nameF = pure name
-- , ageF = pure age
-- , likesDogsF = pure likesDogs
-- }
--
-- partialUser :: UserF Maybe
-- partialUser = UserF
-- { nameF = Just "Tom"
-- , ageF = Nothing
-- , likesDogsF = Just True
-- }
--
-- userInputtedUser :: UserF IO
-- userInputtedUser = UserF
-- { nameF = putStr "Name: " >> getLine
-- , ageF = putStr "Age: " >> fmap read getLine
-- , likesDogsF = putStr "Likes dogs: " >> fmap read getLine
-- }
main :: IO ()
main = putStrLn "Hello, Haskell!"
{-# LANGUAGE DeriveGeneric #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE RecordWildCards #-}
{-# LANGUAGE TypeFamilyDependencies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}
module Main where
import Data.Void (Void)
import Data.Kind (Type)
import GHC.Generics
data User
= User
{ name :: String
, age :: Int
, likesDogs :: Bool
}
deriving (Eq, Generic, Ord, Show)
data UserF (f :: Type -> Type)
= UserF
{ nameF :: f String
, ageF :: f Int
, likesDogsF :: f Bool
}
---
type family GHKDify (rep :: Type -> Type) (f :: Type -> Type)
= (output :: Type -> Type) | output -> rep f where
GHKDify (M1 index metadata inner) f
= M1 index metadata (GHKDify inner f)
GHKDify (left :+: right) f
= GHKDify left f :+: GHKDify right f
GHKDify (left :*: right) f
= GHKDify left f :*: GHKDify right f
GHKDify (K1 R x) f
= K1 R (f x)
newtype HKD (x :: Type) (f :: Type -> Type)
= HKD { runHKD :: GHKDify (Rep x) f Void }
class GConstruction (rep :: Type -> Type) where
gconstruct :: Applicative f => GHKDify rep f p -> f (rep p)
gdestruct :: Applicative f => rep p -> GHKDify rep f p
instance GConstruction inner
=> GConstruction (M1 index meta inner) where
gconstruct (M1 x) = fmap M1 (gconstruct x)
gdestruct (M1 x) = M1 (gdestruct x)
instance (GConstruction left, GConstruction right)
=> GConstruction (left :*: right) where
gconstruct (left :*: right)
= (:*:) <$> gconstruct left <*> gconstruct right
gdestruct (left :*: right)
= gdestruct left :*: gdestruct right
instance GConstruction (K1 R x) where
gconstruct (K1 x) = fmap K1 x
gdestruct (K1 x) = K1 (pure x)
class Construction (x :: Type) where
construct :: Applicative f => HKD x f -> f x
destruct :: Applicative f => x -> HKD x f
instance (Generic x, GConstruction (Rep x))
=> Construction x where
construct (HKD hkd) = fmap to (gconstruct hkd)
destruct x = HKD (gdestruct (from x))
-- $> example
example :: Bool
example = do
let input = ("Tom", 26, True)
construct (destruct input) == Just input
-------------------------------------------------
main :: IO ()
main = putStrLn "Hi, Mum!"
{-# LANGUAGE BlockArguments #-}
{-# LANGUAGE DeriveFunctor #-}
{-# LANGUAGE DerivingVia #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE LambdaCase #-}
import Control.Applicative (liftA2)
import Control.Monad (join)
import Data.IORef (IORef)
import qualified Data.IORef as IORef
import Data.Kind (Type)
import Data.Monoid (Ap (..))
import Prelude hiding (negate, read)
import qualified Prelude as P
-- $> main
main :: IO ()
main = do
x <- make 2
y <- make 3
z <- make 6
w <- unknown
o <- unknown
p <- unknown
add x y z
negate w z
add y w o
negate o p
read p >>= print
add :: Cell Int -> Cell Int -> Cell Int -> IO ()
add x y z = do
binary (+) x y z
binary (-) z y x
binary (-) z x y
negate :: Cell Int -> Cell Int -> IO ()
negate x y = do
unary P.negate x y
unary P.negate y x
--------------------------------------------------
data Defined (x :: Type)
= Undefined -- |
| Exactly x -- |
| Contradiction -- v
deriving (Eq, Ord, Show, Functor)
deriving Num via Ap Defined x
instance Eq x => Semigroup (Defined x) where
Contradiction <> _ = Contradiction
_ <> Contradiction = Contradiction
Exactly x <> Exactly y
| x == y = Exactly x
| otherwise = Contradiction
Undefined <> that = that
this <> Undefined = this
instance Eq x => Monoid (Defined x) where
mempty = Undefined
instance Applicative Defined where
pure = Exactly
liftA2 _ Contradiction _ = Contradiction
liftA2 _ _ Contradiction = Contradiction
liftA2 f (Exactly x) (Exactly y) = Exactly (f x y)
liftA2 _ Undefined _ = Undefined
liftA2 _ _ Undefined = Undefined
--------------------------------------------------
-- "API"
newtype Cell (x :: Type) -- hide constructor
= Cell { toRef :: IORef (Defined x, IO ()) }
make :: x -> IO (Cell x)
make x = fmap Cell (IORef.newIORef (Exactly x, pure ()))
unknown :: IO (Cell x)
unknown = fmap Cell (IORef.newIORef (Undefined, pure ()))
unary :: Eq y => (x -> y) -> Cell x -> Cell y -> IO ()
unary f xs ys = watch xs (write ys . fmap f)
binary :: Eq z => (x -> y -> z) -> Cell x -> Cell y -> Cell z -> IO ()
binary f xs ys zs = do
watch xs \x -> read ys >>= \y -> write zs (liftA2 f x y)
watch ys \y -> read xs >>= \x -> write zs (liftA2 f x y)
--------------------------------------------------
-- "Primitives"
read :: Cell x -> IO (Defined x)
read = fmap fst . IORef.readIORef . toRef
write :: Eq x => Cell x -> Defined x -> IO ()
write (Cell ref) update = do
join $ IORef.atomicModifyIORef' ref \(current, action) -> do
let updated = current <> update
if updated == current
then ((current, action), pure ())
else ((updated, action), action)
watch :: Cell x -> (Defined x -> IO ()) -> IO ()
watch cell@(Cell ref) callback = do
let propagator = read cell >>= callback
join $ IORef.atomicModifyIORef' ref \(current, action) ->
( (current, action *> propagator), propagator )
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment