examples/TuringMachine.hs

   1 {-# OPTIONS_GHC -XModalTypes -dcore-lint -ddump-types -XNoMonomorphismRestriction #-}
   2 module TuringMachine (ProcessNetwork) where
   3 import Prelude hiding (const)
   4
   5 class ProcessNetwork g where
   6   logic         :: (Bool -> Bool -> Bool) -> <[ (Bool,(Bool,())) ~~> Bool ]>@g
   7   delay         :: Bool -> <[       (Bool,())  ~~> Bool ]>@g
   8   <[ select  ]> :: <[ (Bool,(Bool,(Bool,())))  ~~> Bool        ]>@g
   9   <[ switch  ]> :: <[       (Bool,(Bool,()))   ~~> (Bool,Bool) ]>@g
  10   <[ switch' ]> :: <[       (Bool,(Bool,()))   ~~> Bool ]>@g
  11
  12
  13 or  = logic (\x y -> x || y)
  14
  15 not :: ProcessNetwork g => <[ (Bool,())  ~~> Bool ]>@g
  16 not = undefined
  17
  18
  19
  20
  21 -- every time it gets an input it spits out the same output value
  22 const :: ProcessNetwork g => Bool -> <[ (Bool,()) ~~> Bool ]>@g
  23 const = undefined
  24
  25 --
  26 -- VERY IMPORTANT!
  27 --
  28 --      Bool   is the type of booleans in Haskell.
  29 --    <[Bool]> is the type of a process network arc in which EACH TOKEN is a boolean.
  30 --
  31 -- This can lead to some slightly-confusing notation:
  32 --
  33 --    (Bool -> Bool)   is a Haskell function that takes a boolean and
  34 --                     (if it halts) returns a Boolean.
  35 --
  36 --   <[Bool ~~> Bool]> is a process network with an input arc whose
  37 --                     tokens are booleans and an output arc whose
  38 --                     tokens are booleans
  39 --
  40
  41 --
  42 -- Think of Haskell values as being like Ptolemy model parameters!
  43 --
  44
  45 condConst initVal =
  46    <[ \condition -> ~~(const initVal) (switch' condition condition) ]>
  47
  48
  49 --
  50 -- The size of the stack is a natural number; these will be
  51 -- represented as a stream of values using *unary notation* in the
  52 -- following form: the number N is represented as "true" followed by
  53 -- N-many "false" values.
  54 --
  55
  56 --
  57 -- A UnaryNumber is just a stream that we give a particular meaning
  58 -- to.  We're going to get some help here from Haskell's type system
  59 -- by creating another type UnaryNumber, but not telling our code that
  60 -- it's actually the same thing as a Stream.  This prevents us from
  61 -- accidentally using a non-UnaryNumber stream where a UnaryNumber was
  62 -- required!
  63 --
  64 type UnaryNumber = Bool
  65
  66
  67 type IncDec = Bool
  68
  69 counter :: ProcessNetwork g => <[ IncDec ~~> UnaryNumber ]>@g
  70 counter = undefined
  71
  72
  73
  74
  75
  76 -- show myself making a type error
  77
  78
  79 -- Investigate later: automatic translation from <[PeanoStream~~>PeanoStream]> to <[Bool~~>Bool]>
  80
  81 -- show why innocuous Haskell program transforms alter the behavior of PNs